diff options
Diffstat (limited to 'subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts')
-rw-r--r-- | subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts | 341 |
1 files changed, 341 insertions, 0 deletions
diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts new file mode 100644 index 00000000..96be0eea --- /dev/null +++ b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts | |||
@@ -0,0 +1,341 @@ | |||
1 | /** | ||
2 | * @file CodeMirror plugin to highlight indentation | ||
3 | * | ||
4 | * This file is based on the | ||
5 | * [@replit/codemirror-indentation-markers](https://github.com/replit/codemirror-indentation-markers) | ||
6 | * package, which is available under the | ||
7 | * [MIT License](https://github.com/replit/codemirror-indentation-markers/blob/543cc508ca5cef5d8350af23973eb1425e31525c/LICENSE). | ||
8 | * | ||
9 | * The highlighting heuristics were adjusted to make them more suitable | ||
10 | * for logic programming. | ||
11 | * | ||
12 | * @see https://github.com/replit/codemirror-indentation-markers/blob/543cc508ca5cef5d8350af23973eb1425e31525c/src/index.ts | ||
13 | */ | ||
14 | |||
15 | import { getIndentUnit } from '@codemirror/language'; | ||
16 | import { Text, RangeSet, EditorState } from '@codemirror/state'; | ||
17 | import { | ||
18 | ViewPlugin, | ||
19 | Decoration, | ||
20 | EditorView, | ||
21 | WidgetType, | ||
22 | PluginValue, | ||
23 | } from '@codemirror/view'; | ||
24 | |||
25 | export const INDENTATION_MARKER_CLASS = 'cm-indentation-marker'; | ||
26 | |||
27 | export const INDENTATION_MARKER_ACTIVE_CLASS = 'active'; | ||
28 | |||
29 | const indentationMark = Decoration.mark({ | ||
30 | class: INDENTATION_MARKER_CLASS, | ||
31 | tagName: 'span', | ||
32 | }); | ||
33 | |||
34 | const activeIndentationMark = Decoration.mark({ | ||
35 | class: `${INDENTATION_MARKER_CLASS} ${INDENTATION_MARKER_ACTIVE_CLASS}`, | ||
36 | tagName: 'span', | ||
37 | }); | ||
38 | |||
39 | /** | ||
40 | * Widget used to simulate N indentation markers on empty lines. | ||
41 | */ | ||
42 | class IndentationWidget extends WidgetType { | ||
43 | constructor( | ||
44 | readonly numIndent: number, | ||
45 | readonly indentSize: number, | ||
46 | readonly activeIndent?: number, | ||
47 | ) { | ||
48 | super(); | ||
49 | } | ||
50 | |||
51 | override eq(other: IndentationWidget) { | ||
52 | return ( | ||
53 | this.numIndent === other.numIndent && | ||
54 | this.indentSize === other.indentSize && | ||
55 | this.activeIndent === other.activeIndent | ||
56 | ); | ||
57 | } | ||
58 | |||
59 | override toDOM(view: EditorView) { | ||
60 | const indentSize = getIndentUnit(view.state); | ||
61 | |||
62 | const wrapper = document.createElement('span'); | ||
63 | wrapper.style.top = '0'; | ||
64 | wrapper.style.left = '4px'; | ||
65 | wrapper.style.position = 'absolute'; | ||
66 | wrapper.style.pointerEvents = 'none'; | ||
67 | |||
68 | for (let indent = 0; indent < this.numIndent; indent += 1) { | ||
69 | const element = document.createElement('span'); | ||
70 | element.className = INDENTATION_MARKER_CLASS; | ||
71 | element.classList.toggle( | ||
72 | INDENTATION_MARKER_ACTIVE_CLASS, | ||
73 | indent === this.activeIndent, | ||
74 | ); | ||
75 | element.innerHTML = ' '.repeat(indentSize); | ||
76 | wrapper.appendChild(element); | ||
77 | } | ||
78 | |||
79 | return wrapper; | ||
80 | } | ||
81 | } | ||
82 | |||
83 | /** | ||
84 | * Returns the number of indentation markers a non-empty line should have | ||
85 | * based on the text in the line and the size of the indent. | ||
86 | */ | ||
87 | function getNumIndentMarkersForNonEmptyLine( | ||
88 | text: string, | ||
89 | indentSize: number, | ||
90 | onIndentMarker?: (pos: number) => void, | ||
91 | ) { | ||
92 | let numIndents = 0; | ||
93 | let numConsecutiveSpaces = 0; | ||
94 | let prevChar: string | null = null; | ||
95 | |||
96 | for (let char = 0; char < text.length; char += 1) { | ||
97 | // Bail if we encounter a non-whitespace character | ||
98 | if (text[char] !== ' ' && text[char] !== '\t') { | ||
99 | // We still increment the indentation level if we would | ||
100 | // have added a marker here had this been a space or tab. | ||
101 | if (numConsecutiveSpaces % indentSize === 0 && char !== 0) { | ||
102 | numIndents += 1; | ||
103 | } | ||
104 | |||
105 | return numIndents; | ||
106 | } | ||
107 | |||
108 | // Every tab and N space has an indentation marker | ||
109 | const shouldAddIndent = | ||
110 | prevChar === '\t' || numConsecutiveSpaces % indentSize === 0; | ||
111 | |||
112 | if (shouldAddIndent) { | ||
113 | numIndents += 1; | ||
114 | |||
115 | if (onIndentMarker) { | ||
116 | onIndentMarker(char); | ||
117 | } | ||
118 | } | ||
119 | |||
120 | if (text[char] === ' ') { | ||
121 | numConsecutiveSpaces += 1; | ||
122 | } else { | ||
123 | numConsecutiveSpaces = 0; | ||
124 | } | ||
125 | |||
126 | prevChar = text[char]; | ||
127 | } | ||
128 | |||
129 | return numIndents; | ||
130 | } | ||
131 | |||
132 | /** | ||
133 | * Returns the number of indent markers an empty line should have | ||
134 | * based on the number of indent markers of the previous | ||
135 | * and next non-empty lines. | ||
136 | */ | ||
137 | function getNumIndentMarkersForEmptyLine(prev: number, next: number) { | ||
138 | const min = Math.min(prev, next); | ||
139 | const max = Math.max(prev, next); | ||
140 | |||
141 | // If only one side is non-zero, we omit markers, | ||
142 | // because in logic programming, a block often ends with an empty line. | ||
143 | if (min === 0 && max > 0) { | ||
144 | return 0; | ||
145 | } | ||
146 | |||
147 | // Else, default to the minimum of the two | ||
148 | return min; | ||
149 | } | ||
150 | |||
151 | /** | ||
152 | * Returns the next non-empty line and its indent level. | ||
153 | */ | ||
154 | function findNextNonEmptyLineAndIndentLevel( | ||
155 | doc: Text, | ||
156 | startLine: number, | ||
157 | indentSize: number, | ||
158 | ): [number, number] { | ||
159 | const numLines = doc.lines; | ||
160 | let lineNo = startLine; | ||
161 | |||
162 | while (lineNo <= numLines) { | ||
163 | const { text } = doc.line(lineNo); | ||
164 | |||
165 | if (text.trim().length === 0) { | ||
166 | lineNo += 1; | ||
167 | } else { | ||
168 | const indent = getNumIndentMarkersForNonEmptyLine(text, indentSize); | ||
169 | return [lineNo, indent]; | ||
170 | } | ||
171 | } | ||
172 | |||
173 | // Reached the end of the doc | ||
174 | return [numLines + 1, 0]; | ||
175 | } | ||
176 | |||
177 | interface IndentationMarkerDesc { | ||
178 | lineNumber: number; | ||
179 | from: number; | ||
180 | to: number; | ||
181 | create(activeIndentIndex?: number): Decoration; | ||
182 | } | ||
183 | |||
184 | /** | ||
185 | * Returns a range of lines with an active indent marker. | ||
186 | */ | ||
187 | function getLinesWithActiveIndentMarker( | ||
188 | state: EditorState, | ||
189 | indentMap: Map<number, number>, | ||
190 | ): { start: number; end: number; activeIndent: number } { | ||
191 | const currentLine = state.doc.lineAt(state.selection.main.head); | ||
192 | const currentIndent = indentMap.get(currentLine.number); | ||
193 | const currentLineNo = currentLine.number; | ||
194 | |||
195 | if (!currentIndent) { | ||
196 | return { start: -1, end: -1, activeIndent: NaN }; | ||
197 | } | ||
198 | |||
199 | let start: number; | ||
200 | let end: number; | ||
201 | |||
202 | for (start = currentLineNo; start >= 0; start -= 1) { | ||
203 | const indent = indentMap.get(start - 1); | ||
204 | if (!indent || indent < currentIndent) { | ||
205 | break; | ||
206 | } | ||
207 | } | ||
208 | |||
209 | for (end = currentLineNo; ; end += 1) { | ||
210 | const indent = indentMap.get(end + 1); | ||
211 | if (!indent || indent < currentIndent) { | ||
212 | break; | ||
213 | } | ||
214 | } | ||
215 | |||
216 | return { start, end, activeIndent: currentIndent }; | ||
217 | } | ||
218 | /** | ||
219 | * Adds indentation markers to all lines within view. | ||
220 | */ | ||
221 | function addIndentationMarkers(view: EditorView) { | ||
222 | const indentSize = getIndentUnit(view.state); | ||
223 | const indentSizeMap = new Map</* lineNumber */ number, number>(); | ||
224 | const decorations: Array<IndentationMarkerDesc> = []; | ||
225 | |||
226 | view.visibleRanges.forEach(({ from, to }) => { | ||
227 | let pos = from; | ||
228 | |||
229 | let prevIndentMarkers = 0; | ||
230 | let nextIndentMarkers = 0; | ||
231 | let nextNonEmptyLine = 0; | ||
232 | |||
233 | while (pos <= to) { | ||
234 | const line = view.state.doc.lineAt(pos); | ||
235 | const { text } = line; | ||
236 | |||
237 | // If a line is empty, we match the indentation according | ||
238 | // to a heuristic based on the indentations of the | ||
239 | // previous and next non-empty lines. | ||
240 | if (text.trim().length === 0) { | ||
241 | // To retrieve the next non-empty indentation level, | ||
242 | // we perform a lookahead and cache the result. | ||
243 | if (nextNonEmptyLine < line.number) { | ||
244 | const [nextLine, nextIndent] = findNextNonEmptyLineAndIndentLevel( | ||
245 | view.state.doc, | ||
246 | line.number + 1, | ||
247 | indentSize, | ||
248 | ); | ||
249 | |||
250 | nextNonEmptyLine = nextLine; | ||
251 | nextIndentMarkers = nextIndent; | ||
252 | } | ||
253 | |||
254 | const numIndentMarkers = getNumIndentMarkersForEmptyLine( | ||
255 | prevIndentMarkers, | ||
256 | nextIndentMarkers, | ||
257 | ); | ||
258 | |||
259 | // Add the indent widget and move on to next line | ||
260 | indentSizeMap.set(line.number, numIndentMarkers); | ||
261 | decorations.push({ | ||
262 | from: pos, | ||
263 | to: pos, | ||
264 | lineNumber: line.number, | ||
265 | create: (activeIndentIndex) => | ||
266 | Decoration.widget({ | ||
267 | widget: new IndentationWidget( | ||
268 | numIndentMarkers, | ||
269 | indentSize, | ||
270 | activeIndentIndex, | ||
271 | ), | ||
272 | }), | ||
273 | }); | ||
274 | } else { | ||
275 | const indices: Array<number> = []; | ||
276 | |||
277 | prevIndentMarkers = getNumIndentMarkersForNonEmptyLine( | ||
278 | text, | ||
279 | indentSize, | ||
280 | (char) => indices.push(char), | ||
281 | ); | ||
282 | |||
283 | indentSizeMap.set(line.number, indices.length); | ||
284 | decorations.push( | ||
285 | ...indices.map( | ||
286 | (char, i): IndentationMarkerDesc => ({ | ||
287 | from: line.from + char, | ||
288 | to: line.from + char + 1, | ||
289 | lineNumber: line.number, | ||
290 | create: (activeIndentIndex) => | ||
291 | activeIndentIndex === i | ||
292 | ? activeIndentationMark | ||
293 | : indentationMark, | ||
294 | }), | ||
295 | ), | ||
296 | ); | ||
297 | } | ||
298 | |||
299 | // Move on to the next line | ||
300 | pos = line.to + 1; | ||
301 | } | ||
302 | }); | ||
303 | |||
304 | const activeBlockRange = getLinesWithActiveIndentMarker( | ||
305 | view.state, | ||
306 | indentSizeMap, | ||
307 | ); | ||
308 | |||
309 | return RangeSet.of<Decoration>( | ||
310 | Array.from(decorations).map(({ lineNumber, from, to, create }) => { | ||
311 | const activeIndent = | ||
312 | lineNumber >= activeBlockRange.start && | ||
313 | lineNumber <= activeBlockRange.end | ||
314 | ? activeBlockRange.activeIndent - 1 | ||
315 | : undefined; | ||
316 | |||
317 | return { from, to, value: create(activeIndent) }; | ||
318 | }), | ||
319 | true, | ||
320 | ); | ||
321 | } | ||
322 | |||
323 | export default function indentationMarkerViewPlugin() { | ||
324 | return ViewPlugin.define<PluginValue & { decorations: RangeSet<Decoration> }>( | ||
325 | (view) => ({ | ||
326 | decorations: addIndentationMarkers(view), | ||
327 | update(update) { | ||
328 | if ( | ||
329 | update.docChanged || | ||
330 | update.viewportChanged || | ||
331 | update.selectionSet | ||
332 | ) { | ||
333 | this.decorations = addIndentationMarkers(update.view); | ||
334 | } | ||
335 | }, | ||
336 | }), | ||
337 | { | ||
338 | decorations: (v) => v.decorations, | ||
339 | }, | ||
340 | ); | ||
341 | } | ||