tricu

syntax.ts (8628B)

---

 // Presentation only: never used for parsing, compilation, or name resolution.
 // Offsets are UTF-16 textarea offsets, not compiler Unicode-scalar positions.
 export interface Token { start: number; end: number; kind: string; text: string }
 const keywords = new Set(['let', 'in', 'where', 'do', 'case', 'of', 'rec']);
 export function tokenize(source: string): Token[] {
   // Decoration must remain cheap even for large read-only library sources.
   if (source.length > 32_768) return [{ start: 0, end: source.length, kind: '', text: source }];
   const tokens: Token[] = [];
   const add = (start: number, end: number, kind: string): void => { tokens.push({ start, end, kind, text: source.slice(start, end) }); };
   let i = 0;
   while (i < source.length) {
     const start = i, tail = source.slice(i);
     if (tail.startsWith('--')) { const end = source.indexOf('\n', i); i = end < 0 ? source.length : end; add(start, i, 'comment'); }
     else if (tail.startsWith('|-')) { const end = source.indexOf('-|', i + 2); i = end < 0 ? source.length : end + 2; add(start, i, 'comment'); }
     else if (source[i] === '"') {
       i++; let part = start;
       while (i < source.length) {
         if (source[i] === '\\') {
           add(part, i, 'string'); const escape = i; i = Math.min(i + 1 + ((source.codePointAt(i + 1) ?? 0) > 0xffff ? 2 : 1), source.length);
           add(escape, i, /^[\\][ntrfb\\"']$/.test(source.slice(escape, i)) ? 'escape' : 'invalid'); part = i;
         } else if (source[i++] === '"') break;
       }
       if (part < i) add(part, i, 'string');
     } else {
       const match = /^(\s+|![A-Za-z]+|[A-Za-z_][A-Za-z0-9_?'$%.\-]*|[0-9]+|=@|<-|<\||\|>|.)/su.exec(tail)!;
       const text = match[0]; i += text.length;
       const kind = /^\s/.test(text) ? '' : text === 't' ? 'tree' : keywords.has(text) ? 'keyword'
         : ['!import', '!export'].includes(text) ? 'directive' : /^[0-9]/.test(text) ? 'number'
         : /^[A-Za-z_]/.test(text) ? 'name' : /^[()[\]{}]$/.test(text) ? 'bracket' : 'operator';
       add(start, i, kind);
     }
   }
   // Conservative declaration-site recognition, not semantic highlighting.
   // Layout contexts distinguish local equation heads from case-arm captures.
   const significant = tokens.filter(t => t.kind && t.kind !== 'comment');
   const contexts: { kind: string; indent: number; depth: number }[] = [];
   let depth = 0, previous: Token | undefined, directiveLine = -1, line = 0;
   let lineEnd = source.indexOf('\n'); if (lineEnd < 0) lineEnd = source.length;
   let indent = /^ */.exec(source)![0].length;
   for (let n = 0; n < significant.length; n++) {
     const token = significant[n]!;
     while (lineEnd < token.start) {
       line = lineEnd + 1; const next = source.indexOf('\n', line); lineEnd = next < 0 ? source.length : next;
       indent = /^ */.exec(source.slice(line))![0].length;
     }
     const first = token.start === line + indent;
     if (first) while (contexts.length && indent <= contexts.at(-1)!.indent) contexts.pop();
     if (/^[)\]}]$/.test(token.text)) depth--;
     while (contexts.length && depth < contexts.at(-1)!.depth) contexts.pop();
     if (token.kind === 'directive') directiveLine = line;
     if (directiveLine === line && ['as', 'from'].includes(token.text)) token.kind = 'keyword';
     if (token.kind === 'name' && ['@', '=@'].includes(previous?.text ?? '')) token.kind = 'contract';
     const localHead = previous && ['let', 'where', 'rec'].includes(previous.text);
     if (token.kind === 'name' && directiveLine !== line && (localHead || first && (indent === 0 || ['let', 'where'].includes(contexts.at(-1)?.kind ?? '')))) {
       let nesting = 0;
       for (let j = n + 1; j < significant.length; j++) {
         const next = significant[j]!;
         if (next.start > lineEnd || keywords.has(next.text)) break;
         if (nesting === 0 && (next.text === '=' || next.text === '=@')) { token.kind = 'definition'; break; }
         if (/^[([{]$/.test(next.text)) nesting++;
         if (/^[)\]}]$/.test(next.text) && --nesting < 0) break;
         if (!nesting && [':', '<-'].includes(next.text)) break;
       }
     }
     if (['let', 'where', 'of'].includes(token.text)) contexts.push({ kind: token.text, indent, depth });
     if (token.text === 'in') { const index = contexts.map(c => c.kind).lastIndexOf('let'); if (index >= 0) contexts.splice(index); }
     if (/^[([{]$/.test(token.text)) depth++;
     previous = token;
   }
   return tokens;
 }
 
 export function bracketPair(tokens: Token[], caret: number): number[] {
   const brackets = tokens.filter(t => t.kind === 'bracket');
   const selected = brackets.find(t => t.start === caret) ?? brackets.find(t => t.end === caret);
   if (!selected) return [];
   const stack: Token[] = [], pairs = new Map<number, number>();
   for (const token of brackets) {
     if ('([{'.includes(token.text)) stack.push(token);
     else {
       const open = stack.pop();
       if (open && '([{'.indexOf(open.text) === ')]}'.indexOf(token.text)) {
         pairs.set(open.start, token.start); pairs.set(token.start, open.start);
       } else stack.length = 0; // Never match across malformed nesting.
     }
   }
   const partner = pairs.get(selected.start);
   return partner === undefined ? [selected.start] : [selected.start, partner];
 }
 
 export function paintSyntax(target: HTMLElement, tokens: Token[], pair: number[] = []): void {
   const fragment = document.createDocumentFragment();
   for (const token of tokens) {
     if (!token.kind) { fragment.append(document.createTextNode(token.text)); continue; }
     const span = document.createElement('span'); span.className = `syntax-${token.kind}`; span.textContent = token.text;
     if (pair.includes(token.start)) span.classList.add(pair.length === 2 ? 'bracket-match' : 'bracket-unmatched');
     fragment.append(span);
   }
   target.replaceChildren(fragment);
 }
 
 export function syntaxEditor(input: HTMLTextAreaElement): () => void {
   const wrapper = document.createElement('div'); wrapper.className = 'syntax-editor';
   input.before(wrapper); wrapper.append(input);
   const viewport = document.createElement('div'); viewport.className = 'syntax-viewport'; viewport.setAttribute('aria-hidden', 'true');
   const mirror = document.createElement('pre'); viewport.append(mirror); wrapper.prepend(viewport);
   let value: string | undefined, tokens: Token[] = [], lastPair = '', composing = false;
   function scroll(): void { mirror.style.transform = `translate(${-input.scrollLeft}px, ${-input.scrollTop}px)`; }
   function refresh(): void {
     wrapper.hidden = input.hidden;
     wrapper.classList.toggle('modified', input.classList.contains('modified'));
     wrapper.classList.toggle('disabled', input.disabled);
     wrapper.classList.toggle('composing', composing);
     const style = getComputedStyle(input);
     // Use the textarea's actual content box, excluding scrollbar and border.
     mirror.style.width = `${input.clientWidth}px`;
     viewport.style.inset = `${style.borderTopWidth} ${style.borderRightWidth} ${style.borderBottomWidth} ${style.borderLeftWidth}`;
     for (const property of ['font-family', 'font-size', 'line-height', 'font-weight', 'font-style', 'font-stretch', 'font-variant-ligatures', 'font-kerning', 'font-feature-settings', 'font-variation-settings', 'letter-spacing', 'padding', 'tab-size', 'text-align']) mirror.style.setProperty(property, style.getPropertyValue(property));
     const changed = value !== input.value;
     if (changed) { value = input.value; tokens = tokenize(value); }
     const pair = !composing && document.activeElement === input && input.selectionStart === input.selectionEnd ? bracketPair(tokens, input.selectionStart) : [];
     if (changed || pair.join() !== lastPair) {
       paintSyntax(mirror, tokens, pair); lastPair = pair.join();
       // Preserve a trailing empty line without introducing a new line.
       if (!value || value.endsWith('\n')) mirror.append(document.createTextNode(' '));
     }
     scroll();
   }
   input.classList.add('syntax-input');
   for (const event of ['input', 'click', 'keyup', 'select', 'focus', 'blur']) input.addEventListener(event, refresh);
   input.addEventListener('compositionstart', () => { composing = true; refresh(); });
   input.addEventListener('compositionend', () => { composing = false; refresh(); });
   input.addEventListener('scroll', scroll, { passive: true });
   document.addEventListener('selectionchange', () => { if (document.activeElement === input) refresh(); });
   new ResizeObserver(refresh).observe(input);
   new MutationObserver(refresh).observe(input, { attributes: true, attributeFilter: ['hidden', 'disabled', 'class'] });
   refresh(); return refresh;
 }