diff options
author | 2022-10-31 15:57:18 -0400 | |
---|---|---|
committer | 2022-11-05 19:41:17 +0100 | |
commit | 20895372d408e41d2cb929dc7a568afce94807ce (patch) | |
tree | dd192e1d64e5ecec6ec17a72df3f86acbacc5c95 /subprojects/frontend | |
parent | refactor: DNF atoms (diff) | |
download | refinery-20895372d408e41d2cb929dc7a568afce94807ce.tar.gz refinery-20895372d408e41d2cb929dc7a568afce94807ce.tar.zst refinery-20895372d408e41d2cb929dc7a568afce94807ce.zip |
refactor(frontend): editor theme improvements
Diffstat (limited to 'subprojects/frontend')
-rw-r--r-- | subprojects/frontend/src/editor/EditorTheme.ts | 37 | ||||
-rw-r--r-- | subprojects/frontend/src/editor/createEditorState.ts | 2 | ||||
-rw-r--r-- | subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts | 341 |
3 files changed, 370 insertions, 10 deletions
diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index fa77862c..325f8d18 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts | |||
@@ -4,6 +4,11 @@ import infoSVG from '@material-icons/svg/svg/info/baseline.svg?raw'; | |||
4 | import warningSVG from '@material-icons/svg/svg/warning/baseline.svg?raw'; | 4 | import warningSVG from '@material-icons/svg/svg/warning/baseline.svg?raw'; |
5 | import { alpha, styled, type CSSObject } from '@mui/material/styles'; | 5 | import { alpha, styled, type CSSObject } from '@mui/material/styles'; |
6 | 6 | ||
7 | import { | ||
8 | INDENTATION_MARKER_ACTIVE_CLASS, | ||
9 | INDENTATION_MARKER_CLASS, | ||
10 | } from './indentationMarkerViewPlugin'; | ||
11 | |||
7 | function svgURL(svg: string): string { | 12 | function svgURL(svg: string): string { |
8 | return `url('data:image/svg+xml;utf8,${svg}')`; | 13 | return `url('data:image/svg+xml;utf8,${svg}')`; |
9 | } | 14 | } |
@@ -62,6 +67,9 @@ export default styled('div', { | |||
62 | background: theme.palette.highlight.selection, | 67 | background: theme.palette.highlight.selection, |
63 | }, | 68 | }, |
64 | }, | 69 | }, |
70 | '.cm-line': { | ||
71 | position: 'relative', // For indentation highlights | ||
72 | }, | ||
65 | }; | 73 | }; |
66 | 74 | ||
67 | const highlightingStyle: CSSObject = { | 75 | const highlightingStyle: CSSObject = { |
@@ -149,6 +157,13 @@ export default styled('div', { | |||
149 | '.cm-searchMatch-selected': { | 157 | '.cm-searchMatch-selected': { |
150 | background: theme.palette.highlight.search.selected, | 158 | background: theme.palette.highlight.search.selected, |
151 | }, | 159 | }, |
160 | [`.${INDENTATION_MARKER_CLASS}`]: { | ||
161 | display: 'inline-block', | ||
162 | boxShadow: `1px 0 0 ${theme.palette.highlight.lineNumber} inset`, | ||
163 | }, | ||
164 | [`.${INDENTATION_MARKER_CLASS}.${INDENTATION_MARKER_ACTIVE_CLASS}`]: { | ||
165 | boxShadow: `1px 0 0 ${theme.palette.text.primary} inset`, | ||
166 | }, | ||
152 | }; | 167 | }; |
153 | 168 | ||
154 | const lineNumberStyle: CSSObject = { | 169 | const lineNumberStyle: CSSObject = { |
@@ -311,17 +326,7 @@ export default styled('div', { | |||
311 | 326 | ||
312 | const foldStyle = { | 327 | const foldStyle = { |
313 | '.cm-foldGutter': { | 328 | '.cm-foldGutter': { |
314 | opacity: 0, | ||
315 | width: 16, | 329 | width: 16, |
316 | transition: theme.transitions.create('opacity', { | ||
317 | duration: theme.transitions.duration.short, | ||
318 | }), | ||
319 | '@media (hover: none)': { | ||
320 | opacity: 1, | ||
321 | }, | ||
322 | }, | ||
323 | '.cm-gutters:hover .cm-foldGutter': { | ||
324 | opacity: 1, | ||
325 | }, | 330 | }, |
326 | '.problem-editor-foldMarker': { | 331 | '.problem-editor-foldMarker': { |
327 | display: 'block', | 332 | display: 'block', |
@@ -338,6 +343,18 @@ export default styled('div', { | |||
338 | margin: '2px 0', | 343 | margin: '2px 0', |
339 | }, | 344 | }, |
340 | }, | 345 | }, |
346 | '.problem-editor-foldMarker-open': { | ||
347 | opacity: 0, | ||
348 | transition: theme.transitions.create('opacity', { | ||
349 | duration: theme.transitions.duration.short, | ||
350 | }), | ||
351 | '@media (hover: none)': { | ||
352 | opacity: 1, | ||
353 | }, | ||
354 | }, | ||
355 | '.cm-gutters:hover .problem-editor-foldMarker-open': { | ||
356 | opacity: 1, | ||
357 | }, | ||
341 | '.problem-editor-foldMarker-closed': { | 358 | '.problem-editor-foldMarker-closed': { |
342 | transform: 'rotate(-90deg)', | 359 | transform: 'rotate(-90deg)', |
343 | }, | 360 | }, |
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts index c61f4a22..079e8a47 100644 --- a/subprojects/frontend/src/editor/createEditorState.ts +++ b/subprojects/frontend/src/editor/createEditorState.ts | |||
@@ -37,6 +37,7 @@ import problemLanguageSupport from '../language/problemLanguageSupport'; | |||
37 | import type EditorStore from './EditorStore'; | 37 | import type EditorStore from './EditorStore'; |
38 | import SearchPanel from './SearchPanel'; | 38 | import SearchPanel from './SearchPanel'; |
39 | import findOccurrences from './findOccurrences'; | 39 | import findOccurrences from './findOccurrences'; |
40 | import indentationMarkerViewPlugin from './indentationMarkerViewPlugin'; | ||
40 | import semanticHighlighting from './semanticHighlighting'; | 41 | import semanticHighlighting from './semanticHighlighting'; |
41 | 42 | ||
42 | export default function createEditorState( | 43 | export default function createEditorState( |
@@ -60,6 +61,7 @@ export default function createEditorState( | |||
60 | highlightSpecialChars(), | 61 | highlightSpecialChars(), |
61 | history(), | 62 | history(), |
62 | indentOnInput(), | 63 | indentOnInput(), |
64 | indentationMarkerViewPlugin(), | ||
63 | rectangularSelection(), | 65 | rectangularSelection(), |
64 | search({ | 66 | search({ |
65 | createPanel(view) { | 67 | createPanel(view) { |
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 | } | ||