syntax.js (9398B)
1 const keywords = new Set(['let', 'in', 'where', 'do', 'case', 'of', 'rec']); 2 export function tokenize(source) { 3 // Decoration must remain cheap even for large read-only library sources. 4 if (source.length > 32_768) 5 return [{ start: 0, end: source.length, kind: '', text: source }]; 6 const tokens = []; 7 const add = (start, end, kind) => { tokens.push({ start, end, kind, text: source.slice(start, end) }); }; 8 let i = 0; 9 while (i < source.length) { 10 const start = i, tail = source.slice(i); 11 if (tail.startsWith('--')) { 12 const end = source.indexOf('\n', i); 13 i = end < 0 ? source.length : end; 14 add(start, i, 'comment'); 15 } 16 else if (tail.startsWith('|-')) { 17 const end = source.indexOf('-|', i + 2); 18 i = end < 0 ? source.length : end + 2; 19 add(start, i, 'comment'); 20 } 21 else if (source[i] === '"') { 22 i++; 23 let part = start; 24 while (i < source.length) { 25 if (source[i] === '\\') { 26 add(part, i, 'string'); 27 const escape = i; 28 i = Math.min(i + 1 + ((source.codePointAt(i + 1) ?? 0) > 0xffff ? 2 : 1), source.length); 29 add(escape, i, /^[\\][ntrfb\\"']$/.test(source.slice(escape, i)) ? 'escape' : 'invalid'); 30 part = i; 31 } 32 else if (source[i++] === '"') 33 break; 34 } 35 if (part < i) 36 add(part, i, 'string'); 37 } 38 else { 39 const match = /^(\s+|![A-Za-z]+|[A-Za-z_][A-Za-z0-9_?'$%.\-]*|[0-9]+|=@|<-|<\||\|>|.)/su.exec(tail); 40 const text = match[0]; 41 i += text.length; 42 const kind = /^\s/.test(text) ? '' : text === 't' ? 'tree' : keywords.has(text) ? 'keyword' 43 : ['!import', '!export'].includes(text) ? 'directive' : /^[0-9]/.test(text) ? 'number' 44 : /^[A-Za-z_]/.test(text) ? 'name' : /^[()[\]{}]$/.test(text) ? 'bracket' : 'operator'; 45 add(start, i, kind); 46 } 47 } 48 // Conservative declaration-site recognition, not semantic highlighting. 49 // Layout contexts distinguish local equation heads from case-arm captures. 50 const significant = tokens.filter(t => t.kind && t.kind !== 'comment'); 51 const contexts = []; 52 let depth = 0, previous, directiveLine = -1, line = 0; 53 let lineEnd = source.indexOf('\n'); 54 if (lineEnd < 0) 55 lineEnd = source.length; 56 let indent = /^ */.exec(source)[0].length; 57 for (let n = 0; n < significant.length; n++) { 58 const token = significant[n]; 59 while (lineEnd < token.start) { 60 line = lineEnd + 1; 61 const next = source.indexOf('\n', line); 62 lineEnd = next < 0 ? source.length : next; 63 indent = /^ */.exec(source.slice(line))[0].length; 64 } 65 const first = token.start === line + indent; 66 if (first) 67 while (contexts.length && indent <= contexts.at(-1).indent) 68 contexts.pop(); 69 if (/^[)\]}]$/.test(token.text)) 70 depth--; 71 while (contexts.length && depth < contexts.at(-1).depth) 72 contexts.pop(); 73 if (token.kind === 'directive') 74 directiveLine = line; 75 if (directiveLine === line && ['as', 'from'].includes(token.text)) 76 token.kind = 'keyword'; 77 if (token.kind === 'name' && ['@', '=@'].includes(previous?.text ?? '')) 78 token.kind = 'contract'; 79 const localHead = previous && ['let', 'where', 'rec'].includes(previous.text); 80 if (token.kind === 'name' && directiveLine !== line && (localHead || first && (indent === 0 || ['let', 'where'].includes(contexts.at(-1)?.kind ?? '')))) { 81 let nesting = 0; 82 for (let j = n + 1; j < significant.length; j++) { 83 const next = significant[j]; 84 if (next.start > lineEnd || keywords.has(next.text)) 85 break; 86 if (nesting === 0 && (next.text === '=' || next.text === '=@')) { 87 token.kind = 'definition'; 88 break; 89 } 90 if (/^[([{]$/.test(next.text)) 91 nesting++; 92 if (/^[)\]}]$/.test(next.text) && --nesting < 0) 93 break; 94 if (!nesting && [':', '<-'].includes(next.text)) 95 break; 96 } 97 } 98 if (['let', 'where', 'of'].includes(token.text)) 99 contexts.push({ kind: token.text, indent, depth }); 100 if (token.text === 'in') { 101 const index = contexts.map(c => c.kind).lastIndexOf('let'); 102 if (index >= 0) 103 contexts.splice(index); 104 } 105 if (/^[([{]$/.test(token.text)) 106 depth++; 107 previous = token; 108 } 109 return tokens; 110 } 111 export function bracketPair(tokens, caret) { 112 const brackets = tokens.filter(t => t.kind === 'bracket'); 113 const selected = brackets.find(t => t.start === caret) ?? brackets.find(t => t.end === caret); 114 if (!selected) 115 return []; 116 const stack = [], pairs = new Map(); 117 for (const token of brackets) { 118 if ('([{'.includes(token.text)) 119 stack.push(token); 120 else { 121 const open = stack.pop(); 122 if (open && '([{'.indexOf(open.text) === ')]}'.indexOf(token.text)) { 123 pairs.set(open.start, token.start); 124 pairs.set(token.start, open.start); 125 } 126 else 127 stack.length = 0; // Never match across malformed nesting. 128 } 129 } 130 const partner = pairs.get(selected.start); 131 return partner === undefined ? [selected.start] : [selected.start, partner]; 132 } 133 export function paintSyntax(target, tokens, pair = []) { 134 const fragment = document.createDocumentFragment(); 135 for (const token of tokens) { 136 if (!token.kind) { 137 fragment.append(document.createTextNode(token.text)); 138 continue; 139 } 140 const span = document.createElement('span'); 141 span.className = `syntax-${token.kind}`; 142 span.textContent = token.text; 143 if (pair.includes(token.start)) 144 span.classList.add(pair.length === 2 ? 'bracket-match' : 'bracket-unmatched'); 145 fragment.append(span); 146 } 147 target.replaceChildren(fragment); 148 } 149 export function syntaxEditor(input) { 150 const wrapper = document.createElement('div'); 151 wrapper.className = 'syntax-editor'; 152 input.before(wrapper); 153 wrapper.append(input); 154 const viewport = document.createElement('div'); 155 viewport.className = 'syntax-viewport'; 156 viewport.setAttribute('aria-hidden', 'true'); 157 const mirror = document.createElement('pre'); 158 viewport.append(mirror); 159 wrapper.prepend(viewport); 160 let value, tokens = [], lastPair = '', composing = false; 161 function scroll() { mirror.style.transform = `translate(${-input.scrollLeft}px, ${-input.scrollTop}px)`; } 162 function refresh() { 163 wrapper.hidden = input.hidden; 164 wrapper.classList.toggle('modified', input.classList.contains('modified')); 165 wrapper.classList.toggle('disabled', input.disabled); 166 wrapper.classList.toggle('composing', composing); 167 const style = getComputedStyle(input); 168 // Use the textarea's actual content box, excluding scrollbar and border. 169 mirror.style.width = `${input.clientWidth}px`; 170 viewport.style.inset = `${style.borderTopWidth} ${style.borderRightWidth} ${style.borderBottomWidth} ${style.borderLeftWidth}`; 171 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']) 172 mirror.style.setProperty(property, style.getPropertyValue(property)); 173 const changed = value !== input.value; 174 if (changed) { 175 value = input.value; 176 tokens = tokenize(value); 177 } 178 const pair = !composing && document.activeElement === input && input.selectionStart === input.selectionEnd ? bracketPair(tokens, input.selectionStart) : []; 179 if (changed || pair.join() !== lastPair) { 180 paintSyntax(mirror, tokens, pair); 181 lastPair = pair.join(); 182 // Preserve a trailing empty line without introducing a new line. 183 if (!value || value.endsWith('\n')) 184 mirror.append(document.createTextNode(' ')); 185 } 186 scroll(); 187 } 188 input.classList.add('syntax-input'); 189 for (const event of ['input', 'click', 'keyup', 'select', 'focus', 'blur']) 190 input.addEventListener(event, refresh); 191 input.addEventListener('compositionstart', () => { composing = true; refresh(); }); 192 input.addEventListener('compositionend', () => { composing = false; refresh(); }); 193 input.addEventListener('scroll', scroll, { passive: true }); 194 document.addEventListener('selectionchange', () => { if (document.activeElement === input) 195 refresh(); }); 196 new ResizeObserver(refresh).observe(input); 197 new MutationObserver(refresh).observe(input, { attributes: true, attributeFilter: ['hidden', 'disabled', 'class'] }); 198 refresh(); 199 return refresh; 200 }