diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-04-26 20:01:20 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-04-26 20:06:50 +0200 |
commit | a854b1acdef27c54fe008d236282386efc44783e (patch) | |
tree | 7975abaf876db71030a3268bea3e8acf4b0c58fb /subprojects | |
parent | chore(deps): bump dependencies (diff) | |
download | refinery-a854b1acdef27c54fe008d236282386efc44783e.tar.gz refinery-a854b1acdef27c54fe008d236282386efc44783e.tar.zst refinery-a854b1acdef27c54fe008d236282386efc44783e.zip |
fix(web): editor cursor styling
Temporarily remove custom scrollbar and indentation styling, because they
interferred with cursor visibility.
Diffstat (limited to 'subprojects')
4 files changed, 3 insertions, 837 deletions
diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index 023a8f73..e057ce18 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts | |||
@@ -14,32 +14,6 @@ function svgURL(svg: string): string { | |||
14 | return `url('data:image/svg+xml;utf8,${svg}')`; | 14 | return `url('data:image/svg+xml;utf8,${svg}')`; |
15 | } | 15 | } |
16 | 16 | ||
17 | function radialShadowTheme( | ||
18 | origin: string, | ||
19 | scaleX: boolean, | ||
20 | scaleY: boolean, | ||
21 | ): CSSObject { | ||
22 | function radialGradient(opacity: number, scale: string): string { | ||
23 | return `radial-gradient( | ||
24 | farthest-side at ${origin}, | ||
25 | rgba(0, 0, 0, ${opacity}), | ||
26 | rgba(0, 0, 0, 0) | ||
27 | ) | ||
28 | ${origin} / | ||
29 | ${scaleX ? scale : '100%'} | ||
30 | ${scaleY ? scale : '100%'} | ||
31 | no-repeat`; | ||
32 | } | ||
33 | |||
34 | return { | ||
35 | background: ` | ||
36 | ${radialGradient(0.2, '40%')}, | ||
37 | ${radialGradient(0.14, '50%')}, | ||
38 | ${radialGradient(0.12, '100%')} | ||
39 | `, | ||
40 | }; | ||
41 | } | ||
42 | |||
43 | export default styled('div', { | 17 | export default styled('div', { |
44 | name: 'EditorTheme', | 18 | name: 'EditorTheme', |
45 | shouldForwardProp: (propName) => | 19 | shouldForwardProp: (propName) => |
@@ -58,98 +32,13 @@ export default styled('div', { | |||
58 | }, | 32 | }, |
59 | }; | 33 | }; |
60 | 34 | ||
61 | const scrollerThumbOpacity = theme.palette.mode === 'dark' ? 0.16 : 0.28; | ||
62 | |||
63 | const generalStyle: CSSObject = { | 35 | const generalStyle: CSSObject = { |
64 | background: theme.palette.background.default, | 36 | background: theme.palette.background.default, |
65 | '&, .cm-editor': { | 37 | '&, .cm-editor': { |
66 | height: '100%', | 38 | height: '100%', |
67 | }, | 39 | }, |
68 | '.cm-scroller-holder': { | ||
69 | display: 'flex', | ||
70 | position: 'relative', | ||
71 | flexDirection: 'column', | ||
72 | overflow: 'hidden', | ||
73 | flex: '1 1', | ||
74 | }, | ||
75 | '.cm-scroller-spacer': { | ||
76 | position: 'sticky', | ||
77 | flexShrink: 0, | ||
78 | zIndex: 300, | ||
79 | width: 1, | ||
80 | marginRight: -1, | ||
81 | pointerEvents: 'none', | ||
82 | }, | ||
83 | '.cm-scroller': { | 40 | '.cm-scroller': { |
84 | color: theme.palette.text.secondary, | 41 | color: theme.palette.text.secondary, |
85 | scrollbarWidth: 'none', | ||
86 | MsOverflowStyle: 'none', | ||
87 | '&::-webkit-scrollbar': { | ||
88 | width: 0, | ||
89 | height: 0, | ||
90 | background: 'transparent', | ||
91 | }, | ||
92 | }, | ||
93 | '.cm-scroller-track': { | ||
94 | position: 'absolute', | ||
95 | zIndex: 300, | ||
96 | touchAction: 'none', | ||
97 | }, | ||
98 | '.cm-scroller-thumb': { | ||
99 | position: 'absolute', | ||
100 | background: theme.palette.text.secondary, | ||
101 | opacity: scrollerThumbOpacity, | ||
102 | transition: theme.transitions.create('opacity', { | ||
103 | duration: theme.transitions.duration.shortest, | ||
104 | }), | ||
105 | touchAction: 'none', | ||
106 | WebkitTapHighlightColor: 'transparent', | ||
107 | '&:hover': { | ||
108 | opacity: 0.75, | ||
109 | '@media (hover: none)': { | ||
110 | opacity: scrollerThumbOpacity, | ||
111 | }, | ||
112 | }, | ||
113 | '&.active': { | ||
114 | opacity: 1, | ||
115 | pointerEvents: 'none', | ||
116 | userSelect: 'none', | ||
117 | }, | ||
118 | }, | ||
119 | '.cm-scroller-track-y, .cm-scroller-thumb-y': { | ||
120 | top: 0, | ||
121 | right: 0, | ||
122 | width: 12, | ||
123 | }, | ||
124 | '.cm-scroller-track-x, .cm-scroller-thumb-x': { | ||
125 | left: 0, | ||
126 | bottom: 0, | ||
127 | height: 12, | ||
128 | }, | ||
129 | '.cm-scroller-track-x': { | ||
130 | right: 12, | ||
131 | }, | ||
132 | '.cm-scroller-gutter-decoration': { | ||
133 | position: 'absolute', | ||
134 | top: 0, | ||
135 | bottom: 0, | ||
136 | left: 0, | ||
137 | width: 0, | ||
138 | transition: theme.transitions.create('width', { | ||
139 | duration: theme.transitions.duration.shortest, | ||
140 | }), | ||
141 | ...radialShadowTheme('0 50%', true, false), | ||
142 | }, | ||
143 | '.cm-scroller-top-decoration': { | ||
144 | position: 'absolute', | ||
145 | top: 0, | ||
146 | left: 0, | ||
147 | right: 0, | ||
148 | height: 0, | ||
149 | transition: theme.transitions.create('height', { | ||
150 | duration: theme.transitions.duration.shortest, | ||
151 | }), | ||
152 | ...radialShadowTheme('50% 0', false, true), | ||
153 | }, | 42 | }, |
154 | '.cm-gutters': { | 43 | '.cm-gutters': { |
155 | background: theme.palette.background.default, | 44 | background: theme.palette.background.default, |
@@ -168,7 +57,6 @@ export default styled('div', { | |||
168 | background: 'transparent', | 57 | background: 'transparent', |
169 | }, | 58 | }, |
170 | '.cm-cursor, .cm-cursor-primary': { | 59 | '.cm-cursor, .cm-cursor-primary': { |
171 | marginLeft: -1, | ||
172 | borderLeft: `2px solid ${theme.palette.info.main}`, | 60 | borderLeft: `2px solid ${theme.palette.info.main}`, |
173 | }, | 61 | }, |
174 | '.cm-selectionBackground': { | 62 | '.cm-selectionBackground': { |
@@ -181,7 +69,6 @@ export default styled('div', { | |||
181 | }, | 69 | }, |
182 | }, | 70 | }, |
183 | '.cm-line': { | 71 | '.cm-line': { |
184 | position: 'relative', // For indentation highlights | ||
185 | padding: '0 12px 0 0px', | 72 | padding: '0 12px 0 0px', |
186 | }, | 73 | }, |
187 | }; | 74 | }; |
@@ -271,13 +158,6 @@ export default styled('div', { | |||
271 | '.cm-searchMatch-selected': { | 158 | '.cm-searchMatch-selected': { |
272 | background: theme.palette.highlight.search.selected, | 159 | background: theme.palette.highlight.search.selected, |
273 | }, | 160 | }, |
274 | '.cm-indentation-marker': { | ||
275 | display: 'inline-block', | ||
276 | boxShadow: `1px 0 0 ${theme.palette.text.disabled} inset`, | ||
277 | '&.active': { | ||
278 | boxShadow: `1px 0 0 ${theme.palette.text.primary} inset`, | ||
279 | }, | ||
280 | }, | ||
281 | '.cm-scroller-selection': { | 161 | '.cm-scroller-selection': { |
282 | position: 'absolute', | 162 | position: 'absolute', |
283 | right: 0, | 163 | right: 0, |
@@ -458,11 +338,11 @@ export default styled('div', { | |||
458 | 338 | ||
459 | const foldStyle = { | 339 | const foldStyle = { |
460 | '.cm-foldGutter': { | 340 | '.cm-foldGutter': { |
461 | width: 17, | 341 | width: 16, |
462 | }, | 342 | }, |
463 | '.problem-editor-foldMarker': { | 343 | '.problem-editor-foldMarker': { |
464 | display: 'block', | 344 | display: 'block', |
465 | margin: '4px 1px 4px 0', | 345 | margin: '4px 0 4px 0', |
466 | padding: 0, | 346 | padding: 0, |
467 | maskImage: svgURL(expandMoreSVG), | 347 | maskImage: svgURL(expandMoreSVG), |
468 | maskSize: '16px 16px', | 348 | maskSize: '16px 16px', |
@@ -473,7 +353,7 @@ export default styled('div', { | |||
473 | cursor: 'pointer', | 353 | cursor: 'pointer', |
474 | WebkitTapHighlightColor: 'transparent', | 354 | WebkitTapHighlightColor: 'transparent', |
475 | [theme.breakpoints.down('sm')]: { | 355 | [theme.breakpoints.down('sm')]: { |
476 | margin: '2px 1px 2px 0', | 356 | margin: '2px 0 2px 0', |
477 | }, | 357 | }, |
478 | }, | 358 | }, |
479 | '.problem-editor-foldMarker-open': { | 359 | '.problem-editor-foldMarker-open': { |
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts index 4a8e9832..67b8fb9e 100644 --- a/subprojects/frontend/src/editor/createEditorState.ts +++ b/subprojects/frontend/src/editor/createEditorState.ts | |||
@@ -44,8 +44,6 @@ import type EditorStore from './EditorStore'; | |||
44 | import SearchPanel from './SearchPanel'; | 44 | import SearchPanel from './SearchPanel'; |
45 | import exposeDiagnostics from './exposeDiagnostics'; | 45 | import exposeDiagnostics from './exposeDiagnostics'; |
46 | import findOccurrences from './findOccurrences'; | 46 | import findOccurrences from './findOccurrences'; |
47 | import indentationMarkerViewPlugin from './indentationMarkerViewPlugin'; | ||
48 | import scrollbarViewPlugin from './scrollbarViewPlugin'; | ||
49 | import semanticHighlighting from './semanticHighlighting'; | 47 | import semanticHighlighting from './semanticHighlighting'; |
50 | 48 | ||
51 | export default function createEditorState( | 49 | export default function createEditorState( |
@@ -70,7 +68,6 @@ export default function createEditorState( | |||
70 | highlightSpecialChars(), | 68 | highlightSpecialChars(), |
71 | history(), | 69 | history(), |
72 | indentOnInput(), | 70 | indentOnInput(), |
73 | indentationMarkerViewPlugin(), | ||
74 | rectangularSelection(), | 71 | rectangularSelection(), |
75 | search({ | 72 | search({ |
76 | createPanel(view) { | 73 | createPanel(view) { |
@@ -129,7 +126,6 @@ export default function createEditorState( | |||
129 | ...defaultKeymap, | 126 | ...defaultKeymap, |
130 | ]), | 127 | ]), |
131 | problemLanguageSupport(), | 128 | problemLanguageSupport(), |
132 | scrollbarViewPlugin(store), | ||
133 | ], | 129 | ], |
134 | }); | 130 | }); |
135 | } | 131 | } |
diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts deleted file mode 100644 index 57a946d5..00000000 --- a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts +++ /dev/null | |||
@@ -1,347 +0,0 @@ | |||
1 | /* | ||
2 | * Copyright (c) 2022 Replit | ||
3 | * Copyright (c) 2022-2023 The Refinery Authors <https://refinery.tools/> | ||
4 | * | ||
5 | * SPDX-License-Identifier: MIT OR EPL-2.0 | ||
6 | */ | ||
7 | |||
8 | /** | ||
9 | * @file CodeMirror plugin to highlight indentation | ||
10 | * | ||
11 | * This file is based on the | ||
12 | * [@replit/codemirror-indentation-markers](https://github.com/replit/codemirror-indentation-markers) | ||
13 | * package. | ||
14 | * | ||
15 | * The highlighting heuristics were adjusted to make them more suitable | ||
16 | * for logic programming. | ||
17 | * | ||
18 | * @see https://github.com/replit/codemirror-indentation-markers/blob/543cc508ca5cef5d8350af23973eb1425e31525c/src/index.ts | ||
19 | */ | ||
20 | |||
21 | import { getIndentUnit } from '@codemirror/language'; | ||
22 | import { Text, RangeSet, EditorState } from '@codemirror/state'; | ||
23 | import { | ||
24 | ViewPlugin, | ||
25 | Decoration, | ||
26 | EditorView, | ||
27 | WidgetType, | ||
28 | PluginValue, | ||
29 | } from '@codemirror/view'; | ||
30 | |||
31 | export const INDENTATION_MARKER_CLASS = 'cm-indentation-marker'; | ||
32 | |||
33 | export const INDENTATION_MARKER_ACTIVE_CLASS = 'active'; | ||
34 | |||
35 | const indentationMark = Decoration.mark({ | ||
36 | class: INDENTATION_MARKER_CLASS, | ||
37 | tagName: 'span', | ||
38 | }); | ||
39 | |||
40 | const activeIndentationMark = Decoration.mark({ | ||
41 | class: `${INDENTATION_MARKER_CLASS} ${INDENTATION_MARKER_ACTIVE_CLASS}`, | ||
42 | tagName: 'span', | ||
43 | }); | ||
44 | |||
45 | /** | ||
46 | * Widget used to simulate N indentation markers on empty lines. | ||
47 | */ | ||
48 | class IndentationWidget extends WidgetType { | ||
49 | constructor( | ||
50 | readonly numIndent: number, | ||
51 | readonly indentSize: number, | ||
52 | readonly activeIndent?: number, | ||
53 | ) { | ||
54 | super(); | ||
55 | } | ||
56 | |||
57 | override eq(other: IndentationWidget) { | ||
58 | return ( | ||
59 | this.numIndent === other.numIndent && | ||
60 | this.indentSize === other.indentSize && | ||
61 | this.activeIndent === other.activeIndent | ||
62 | ); | ||
63 | } | ||
64 | |||
65 | override toDOM(view: EditorView) { | ||
66 | const indentSize = getIndentUnit(view.state); | ||
67 | |||
68 | const wrapper = document.createElement('span'); | ||
69 | wrapper.style.top = '0'; | ||
70 | wrapper.style.left = '0'; | ||
71 | wrapper.style.position = 'absolute'; | ||
72 | wrapper.style.pointerEvents = 'none'; | ||
73 | |||
74 | for (let indent = 0; indent < this.numIndent; indent += 1) { | ||
75 | const element = document.createElement('span'); | ||
76 | element.className = INDENTATION_MARKER_CLASS; | ||
77 | element.classList.toggle( | ||
78 | INDENTATION_MARKER_ACTIVE_CLASS, | ||
79 | indent === this.activeIndent, | ||
80 | ); | ||
81 | element.innerHTML = ' '.repeat(indentSize); | ||
82 | wrapper.appendChild(element); | ||
83 | } | ||
84 | |||
85 | return wrapper; | ||
86 | } | ||
87 | } | ||
88 | |||
89 | /** | ||
90 | * Returns the number of indentation markers a non-empty line should have | ||
91 | * based on the text in the line and the size of the indent. | ||
92 | */ | ||
93 | function getNumIndentMarkersForNonEmptyLine( | ||
94 | text: string, | ||
95 | indentSize: number, | ||
96 | onIndentMarker?: (pos: number) => void, | ||
97 | ) { | ||
98 | let numIndents = 0; | ||
99 | let numConsecutiveSpaces = 0; | ||
100 | let prevChar: string | undefined; | ||
101 | |||
102 | for (let char = 0; char < text.length; char += 1) { | ||
103 | // Bail if we encounter a non-whitespace character | ||
104 | if (text[char] !== ' ' && text[char] !== '\t') { | ||
105 | // We still increment the indentation level if we would | ||
106 | // have added a marker here had this been a space or tab. | ||
107 | if (numConsecutiveSpaces % indentSize === 0 && char !== 0) { | ||
108 | numIndents += 1; | ||
109 | } | ||
110 | |||
111 | return numIndents; | ||
112 | } | ||
113 | |||
114 | // Every tab and N space has an indentation marker | ||
115 | const shouldAddIndent = | ||
116 | prevChar === '\t' || numConsecutiveSpaces % indentSize === 0; | ||
117 | |||
118 | if (shouldAddIndent) { | ||
119 | numIndents += 1; | ||
120 | |||
121 | if (onIndentMarker) { | ||
122 | onIndentMarker(char); | ||
123 | } | ||
124 | } | ||
125 | |||
126 | if (text[char] === ' ') { | ||
127 | numConsecutiveSpaces += 1; | ||
128 | } else { | ||
129 | numConsecutiveSpaces = 0; | ||
130 | } | ||
131 | |||
132 | prevChar = text[char]; | ||
133 | } | ||
134 | |||
135 | return numIndents; | ||
136 | } | ||
137 | |||
138 | /** | ||
139 | * Returns the number of indent markers an empty line should have | ||
140 | * based on the number of indent markers of the previous | ||
141 | * and next non-empty lines. | ||
142 | */ | ||
143 | function getNumIndentMarkersForEmptyLine(prev: number, next: number) { | ||
144 | const min = Math.min(prev, next); | ||
145 | const max = Math.max(prev, next); | ||
146 | |||
147 | // If only one side is non-zero, we omit markers, | ||
148 | // because in logic programming, a block often ends with an empty line. | ||
149 | if (min === 0 && max > 0) { | ||
150 | return 0; | ||
151 | } | ||
152 | |||
153 | // Else, default to the minimum of the two | ||
154 | return min; | ||
155 | } | ||
156 | |||
157 | /** | ||
158 | * Returns the next non-empty line and its indent level. | ||
159 | */ | ||
160 | function findNextNonEmptyLineAndIndentLevel( | ||
161 | doc: Text, | ||
162 | startLine: number, | ||
163 | indentSize: number, | ||
164 | ): [number, number] { | ||
165 | const numLines = doc.lines; | ||
166 | let lineNo = startLine; | ||
167 | |||
168 | while (lineNo <= numLines) { | ||
169 | const { text } = doc.line(lineNo); | ||
170 | |||
171 | if (text.trim().length === 0) { | ||
172 | lineNo += 1; | ||
173 | } else { | ||
174 | const indent = getNumIndentMarkersForNonEmptyLine(text, indentSize); | ||
175 | return [lineNo, indent]; | ||
176 | } | ||
177 | } | ||
178 | |||
179 | // Reached the end of the doc | ||
180 | return [numLines + 1, 0]; | ||
181 | } | ||
182 | |||
183 | interface IndentationMarkerDesc { | ||
184 | lineNumber: number; | ||
185 | from: number; | ||
186 | to: number; | ||
187 | create(activeIndentIndex?: number): Decoration; | ||
188 | } | ||
189 | |||
190 | /** | ||
191 | * Returns a range of lines with an active indent marker. | ||
192 | */ | ||
193 | function getLinesWithActiveIndentMarker( | ||
194 | state: EditorState, | ||
195 | indentMap: Map<number, number>, | ||
196 | ): { start: number; end: number; activeIndent: number } { | ||
197 | const currentLine = state.doc.lineAt(state.selection.main.head); | ||
198 | const currentIndent = indentMap.get(currentLine.number); | ||
199 | const currentLineNo = currentLine.number; | ||
200 | |||
201 | if (!currentIndent) { | ||
202 | return { start: -1, end: -1, activeIndent: NaN }; | ||
203 | } | ||
204 | |||
205 | let start: number; | ||
206 | let end: number; | ||
207 | |||
208 | for (start = currentLineNo; start >= 0; start -= 1) { | ||
209 | const indent = indentMap.get(start - 1); | ||
210 | if (!indent || indent < currentIndent) { | ||
211 | break; | ||
212 | } | ||
213 | } | ||
214 | |||
215 | for (end = currentLineNo; ; end += 1) { | ||
216 | const indent = indentMap.get(end + 1); | ||
217 | if (!indent || indent < currentIndent) { | ||
218 | break; | ||
219 | } | ||
220 | } | ||
221 | |||
222 | return { start, end, activeIndent: currentIndent }; | ||
223 | } | ||
224 | /** | ||
225 | * Adds indentation markers to all lines within view. | ||
226 | */ | ||
227 | function addIndentationMarkers(view: EditorView) { | ||
228 | const indentSize = getIndentUnit(view.state); | ||
229 | const indentSizeMap = new Map</* lineNumber */ number, number>(); | ||
230 | const decorations: Array<IndentationMarkerDesc> = []; | ||
231 | |||
232 | view.visibleRanges.forEach(({ from, to }) => { | ||
233 | let pos = from; | ||
234 | |||
235 | let prevIndentMarkers = 0; | ||
236 | let nextIndentMarkers = 0; | ||
237 | let nextNonEmptyLine = 0; | ||
238 | |||
239 | while (pos <= to) { | ||
240 | const line = view.state.doc.lineAt(pos); | ||
241 | const { text } = line; | ||
242 | |||
243 | // If a line is empty, we match the indentation according | ||
244 | // to a heuristic based on the indentations of the | ||
245 | // previous and next non-empty lines. | ||
246 | if (text.trim().length === 0) { | ||
247 | // To retrieve the next non-empty indentation level, | ||
248 | // we perform a lookahead and cache the result. | ||
249 | if (nextNonEmptyLine < line.number) { | ||
250 | const [nextLine, nextIndent] = findNextNonEmptyLineAndIndentLevel( | ||
251 | view.state.doc, | ||
252 | line.number + 1, | ||
253 | indentSize, | ||
254 | ); | ||
255 | |||
256 | nextNonEmptyLine = nextLine; | ||
257 | nextIndentMarkers = nextIndent; | ||
258 | } | ||
259 | |||
260 | const numIndentMarkers = getNumIndentMarkersForEmptyLine( | ||
261 | prevIndentMarkers, | ||
262 | nextIndentMarkers, | ||
263 | ); | ||
264 | |||
265 | // Add the indent widget and move on to next line | ||
266 | indentSizeMap.set(line.number, numIndentMarkers); | ||
267 | decorations.push({ | ||
268 | from: pos, | ||
269 | to: pos, | ||
270 | lineNumber: line.number, | ||
271 | create: (activeIndentIndex) => | ||
272 | Decoration.widget({ | ||
273 | widget: new IndentationWidget( | ||
274 | numIndentMarkers, | ||
275 | indentSize, | ||
276 | activeIndentIndex, | ||
277 | ), | ||
278 | }), | ||
279 | }); | ||
280 | } else { | ||
281 | const indices: Array<number> = []; | ||
282 | |||
283 | prevIndentMarkers = getNumIndentMarkersForNonEmptyLine( | ||
284 | text, | ||
285 | indentSize, | ||
286 | (char) => indices.push(char), | ||
287 | ); | ||
288 | |||
289 | indentSizeMap.set(line.number, indices.length); | ||
290 | decorations.push( | ||
291 | ...indices.map( | ||
292 | (char, i): IndentationMarkerDesc => ({ | ||
293 | from: line.from + char, | ||
294 | to: line.from + char + 1, | ||
295 | lineNumber: line.number, | ||
296 | create: (activeIndentIndex) => | ||
297 | activeIndentIndex === i | ||
298 | ? activeIndentationMark | ||
299 | : indentationMark, | ||
300 | }), | ||
301 | ), | ||
302 | ); | ||
303 | } | ||
304 | |||
305 | // Move on to the next line | ||
306 | pos = line.to + 1; | ||
307 | } | ||
308 | }); | ||
309 | |||
310 | const activeBlockRange = getLinesWithActiveIndentMarker( | ||
311 | view.state, | ||
312 | indentSizeMap, | ||
313 | ); | ||
314 | |||
315 | return RangeSet.of<Decoration>( | ||
316 | Array.from(decorations).map(({ lineNumber, from, to, create }) => { | ||
317 | const activeIndent = | ||
318 | lineNumber >= activeBlockRange.start && | ||
319 | lineNumber <= activeBlockRange.end | ||
320 | ? activeBlockRange.activeIndent - 1 | ||
321 | : undefined; | ||
322 | |||
323 | return { from, to, value: create(activeIndent) }; | ||
324 | }), | ||
325 | true, | ||
326 | ); | ||
327 | } | ||
328 | |||
329 | export default function indentationMarkerViewPlugin() { | ||
330 | return ViewPlugin.define<PluginValue & { decorations: RangeSet<Decoration> }>( | ||
331 | (view) => ({ | ||
332 | decorations: addIndentationMarkers(view), | ||
333 | update(update) { | ||
334 | if ( | ||
335 | update.docChanged || | ||
336 | update.viewportChanged || | ||
337 | update.selectionSet | ||
338 | ) { | ||
339 | this.decorations = addIndentationMarkers(update.view); | ||
340 | } | ||
341 | }, | ||
342 | }), | ||
343 | { | ||
344 | decorations: (v) => v.decorations, | ||
345 | }, | ||
346 | ); | ||
347 | } | ||
diff --git a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts b/subprojects/frontend/src/editor/scrollbarViewPlugin.ts deleted file mode 100644 index 878d369d..00000000 --- a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts +++ /dev/null | |||
@@ -1,363 +0,0 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
7 | import { EditorSelection } from '@codemirror/state'; | ||
8 | import { | ||
9 | type EditorView, | ||
10 | type PluginValue, | ||
11 | ViewPlugin, | ||
12 | } from '@codemirror/view'; | ||
13 | import { reaction } from 'mobx'; | ||
14 | |||
15 | import type EditorStore from './EditorStore'; | ||
16 | import { getDiagnostics } from './exposeDiagnostics'; | ||
17 | import findOccurrences from './findOccurrences'; | ||
18 | |||
19 | export const HOLDER_CLASS = 'cm-scroller-holder'; | ||
20 | export const SPACER_CLASS = 'cm-scroller-spacer'; | ||
21 | export const TRACK_CLASS = 'cm-scroller-track'; | ||
22 | export const THUMB_CLASS = 'cm-scroller-thumb'; | ||
23 | export const THUMB_ACTIVE_CLASS = 'active'; | ||
24 | export const GUTTER_DECORATION_CLASS = 'cm-scroller-gutter-decoration'; | ||
25 | export const TOP_DECORATION_CLASS = 'cm-scroller-top-decoration'; | ||
26 | export const ANNOTATION_SELECTION_CLASS = 'cm-scroller-selection'; | ||
27 | export const ANNOTATION_DIAGNOSTIC_CLASS = 'cm-scroller-diagnostic'; | ||
28 | export const ANNOTATION_OCCURRENCE_CLASS = 'cm-scroller-occurrence'; | ||
29 | export const SHADOW_WIDTH = 10; | ||
30 | export const SCROLLBAR_WIDTH = 12; | ||
31 | export const ANNOTATION_WIDTH = SCROLLBAR_WIDTH / 2; | ||
32 | export const MIN_ANNOTATION_HEIGHT = 1; | ||
33 | |||
34 | function createScrollbar( | ||
35 | holder: HTMLElement, | ||
36 | direction: 'x' | 'y', | ||
37 | touchCallback: (offsetX: number, offsetY: number) => void, | ||
38 | moveCallback: (movementX: number, movementY: number) => void, | ||
39 | ): { track: HTMLElement; thumb: HTMLElement } { | ||
40 | const track = holder.ownerDocument.createElement('div'); | ||
41 | track.className = `${TRACK_CLASS} ${TRACK_CLASS}-${direction}`; | ||
42 | holder.appendChild(track); | ||
43 | |||
44 | const thumb = holder.ownerDocument.createElement('div'); | ||
45 | thumb.className = `${THUMB_CLASS} ${THUMB_CLASS}-${direction}`; | ||
46 | track.appendChild(thumb); | ||
47 | |||
48 | let pointerId: number | undefined; | ||
49 | track.addEventListener('pointerdown', (event) => { | ||
50 | if (pointerId !== undefined) { | ||
51 | event.preventDefault(); | ||
52 | return; | ||
53 | } | ||
54 | ({ pointerId } = event); | ||
55 | thumb.classList.add(THUMB_ACTIVE_CLASS); | ||
56 | if (event.target === thumb) { | ||
57 | // Prevent implicit pointer capture on mobile. | ||
58 | thumb.releasePointerCapture(pointerId); | ||
59 | } else { | ||
60 | touchCallback(event.offsetX, event.offsetY); | ||
61 | } | ||
62 | track.setPointerCapture(pointerId); | ||
63 | }); | ||
64 | |||
65 | track.addEventListener('pointermove', (event) => { | ||
66 | if (event.pointerId !== pointerId) { | ||
67 | return; | ||
68 | } | ||
69 | moveCallback(event.movementX, event.movementY); | ||
70 | event.preventDefault(); | ||
71 | }); | ||
72 | |||
73 | function scrollEnd(event: PointerEvent) { | ||
74 | if (event.pointerId !== pointerId) { | ||
75 | return; | ||
76 | } | ||
77 | pointerId = undefined; | ||
78 | thumb.classList.remove(THUMB_ACTIVE_CLASS); | ||
79 | } | ||
80 | |||
81 | track.addEventListener('pointerup', scrollEnd, { passive: true }); | ||
82 | track.addEventListener('pointercancel', scrollEnd, { passive: true }); | ||
83 | |||
84 | return { track, thumb }; | ||
85 | } | ||
86 | |||
87 | function rebuildAnnotations( | ||
88 | view: EditorView, | ||
89 | scrollHeight: number, | ||
90 | trackYHeight: number, | ||
91 | holder: HTMLElement, | ||
92 | annotations: HTMLDivElement[], | ||
93 | ) { | ||
94 | const { state } = view; | ||
95 | const overlayAnnotationsHeight = | ||
96 | (view.contentHeight / scrollHeight) * trackYHeight; | ||
97 | const lineHeight = overlayAnnotationsHeight / state.doc.lines; | ||
98 | |||
99 | let i = 0; | ||
100 | |||
101 | function getOrCreateAnnotation(from: number, to?: number): HTMLDivElement { | ||
102 | const startLine = state.doc.lineAt(from).number; | ||
103 | const endLine = to === undefined ? startLine : state.doc.lineAt(to).number; | ||
104 | const top = (startLine - 1) * lineHeight; | ||
105 | const height = Math.max( | ||
106 | MIN_ANNOTATION_HEIGHT, | ||
107 | Math.max(1, endLine - startLine) * lineHeight, | ||
108 | ); | ||
109 | |||
110 | let annotation: HTMLDivElement | undefined; | ||
111 | if (i < annotations.length) { | ||
112 | annotation = annotations[i]; | ||
113 | } | ||
114 | if (annotation === undefined) { | ||
115 | annotation = holder.ownerDocument.createElement('div'); | ||
116 | annotations.push(annotation); | ||
117 | holder.appendChild(annotation); | ||
118 | } | ||
119 | i += 1; | ||
120 | |||
121 | annotation.style.top = `${top}px`; | ||
122 | annotation.style.height = `${height}px`; | ||
123 | |||
124 | return annotation; | ||
125 | } | ||
126 | |||
127 | state.selection.ranges.forEach(({ head }) => { | ||
128 | const selectionAnnotation = getOrCreateAnnotation(head); | ||
129 | selectionAnnotation.className = ANNOTATION_SELECTION_CLASS; | ||
130 | selectionAnnotation.style.width = `${SCROLLBAR_WIDTH}px`; | ||
131 | }); | ||
132 | |||
133 | const diagnosticsIter = getDiagnostics(state).iter(); | ||
134 | while (diagnosticsIter.value !== null) { | ||
135 | const diagnosticAnnotation = getOrCreateAnnotation( | ||
136 | diagnosticsIter.from, | ||
137 | diagnosticsIter.to, | ||
138 | ); | ||
139 | diagnosticAnnotation.className = `${ANNOTATION_DIAGNOSTIC_CLASS} ${ANNOTATION_DIAGNOSTIC_CLASS}-${diagnosticsIter.value.severity}`; | ||
140 | diagnosticAnnotation.style.width = `${ANNOTATION_WIDTH}px`; | ||
141 | diagnosticsIter.next(); | ||
142 | } | ||
143 | |||
144 | const occurrences = view.state.field(findOccurrences); | ||
145 | const occurrencesIter = occurrences.iter(); | ||
146 | while (occurrencesIter.value !== null) { | ||
147 | const occurrenceAnnotation = getOrCreateAnnotation( | ||
148 | occurrencesIter.from, | ||
149 | occurrencesIter.to, | ||
150 | ); | ||
151 | occurrenceAnnotation.className = ANNOTATION_OCCURRENCE_CLASS; | ||
152 | occurrenceAnnotation.style.width = `${ANNOTATION_WIDTH}px`; | ||
153 | occurrenceAnnotation.style.right = `${ANNOTATION_WIDTH}px`; | ||
154 | occurrencesIter.next(); | ||
155 | } | ||
156 | |||
157 | annotations | ||
158 | .splice(i) | ||
159 | .forEach((staleAnnotation) => holder.removeChild(staleAnnotation)); | ||
160 | } | ||
161 | |||
162 | export default function scrollbarViewPlugin( | ||
163 | editorStore: EditorStore, | ||
164 | ): ViewPlugin<PluginValue> { | ||
165 | return ViewPlugin.define((view) => { | ||
166 | const { scrollDOM } = view; | ||
167 | const { ownerDocument, parentElement: parentDOM } = scrollDOM; | ||
168 | if (parentDOM === null) { | ||
169 | return {}; | ||
170 | } | ||
171 | |||
172 | const holder = ownerDocument.createElement('div'); | ||
173 | holder.className = HOLDER_CLASS; | ||
174 | parentDOM.replaceChild(holder, scrollDOM); | ||
175 | holder.appendChild(scrollDOM); | ||
176 | |||
177 | const spacer = ownerDocument.createElement('div'); | ||
178 | spacer.className = SPACER_CLASS; | ||
179 | scrollDOM.insertBefore(spacer, scrollDOM.firstChild); | ||
180 | |||
181 | let gutterWidth = 0; | ||
182 | |||
183 | scrollDOM.addEventListener('click', (event) => { | ||
184 | const scrollX = scrollDOM.scrollLeft + event.offsetX; | ||
185 | const scrollY = scrollDOM.scrollTop + event.offsetY; | ||
186 | if (scrollX > gutterWidth && scrollY > view.contentHeight) { | ||
187 | event.preventDefault(); | ||
188 | view.focus(); | ||
189 | editorStore.dispatch({ | ||
190 | scrollIntoView: true, | ||
191 | selection: EditorSelection.create([ | ||
192 | EditorSelection.cursor(view.state.doc.length), | ||
193 | ]), | ||
194 | }); | ||
195 | } | ||
196 | }); | ||
197 | |||
198 | let factorY = 1; | ||
199 | let factorX = 1; | ||
200 | |||
201 | const { track: trackY, thumb: thumbY } = createScrollbar( | ||
202 | holder, | ||
203 | 'y', | ||
204 | (_offsetX, offsetY) => { | ||
205 | const scaledOffset = offsetY / factorY; | ||
206 | const { height: scrollerHeight } = scrollDOM.getBoundingClientRect(); | ||
207 | const target = Math.max(0, scaledOffset - scrollerHeight / 2); | ||
208 | scrollDOM.scrollTo({ top: target }); | ||
209 | }, | ||
210 | (_movementX, movementY) => { | ||
211 | scrollDOM.scrollBy({ top: movementY / factorY }); | ||
212 | }, | ||
213 | ); | ||
214 | |||
215 | const { track: trackX, thumb: thumbX } = createScrollbar( | ||
216 | holder, | ||
217 | 'x', | ||
218 | (offsetX) => { | ||
219 | const scaledOffset = offsetX / factorX; | ||
220 | const { width: scrollerWidth } = scrollDOM.getBoundingClientRect(); | ||
221 | const target = Math.max(0, scaledOffset - scrollerWidth / 2); | ||
222 | scrollDOM.scrollTo({ left: target }); | ||
223 | }, | ||
224 | (movementX) => { | ||
225 | scrollDOM.scrollBy({ left: movementX / factorX }); | ||
226 | }, | ||
227 | ); | ||
228 | |||
229 | const gutterDecoration = ownerDocument.createElement('div'); | ||
230 | gutterDecoration.className = GUTTER_DECORATION_CLASS; | ||
231 | holder.appendChild(gutterDecoration); | ||
232 | |||
233 | const topDecoration = ownerDocument.createElement('div'); | ||
234 | topDecoration.className = TOP_DECORATION_CLASS; | ||
235 | holder.appendChild(topDecoration); | ||
236 | |||
237 | const disposePanelReaction = reaction( | ||
238 | () => editorStore.searchPanel.state, | ||
239 | (panelOpen) => { | ||
240 | topDecoration.style.display = panelOpen ? 'none' : 'block'; | ||
241 | }, | ||
242 | { fireImmediately: true }, | ||
243 | ); | ||
244 | |||
245 | let gutters: Element | undefined; | ||
246 | |||
247 | let firstRun = true; | ||
248 | let firstRunTimeout: number | undefined; | ||
249 | let requested = false; | ||
250 | let rebuildRequested = false; | ||
251 | |||
252 | const annotations: HTMLDivElement[] = []; | ||
253 | |||
254 | let observer: ResizeObserver | undefined; | ||
255 | |||
256 | function update() { | ||
257 | requested = false; | ||
258 | |||
259 | if (gutters === undefined) { | ||
260 | gutters = scrollDOM.querySelector('.cm-gutters') ?? undefined; | ||
261 | if (gutters !== undefined && observer !== undefined) { | ||
262 | observer.observe(gutters); | ||
263 | } | ||
264 | } | ||
265 | |||
266 | const { height: scrollerHeight, width: scrollerWidth } = | ||
267 | scrollDOM.getBoundingClientRect(); | ||
268 | const { scrollTop, scrollLeft, scrollWidth } = scrollDOM; | ||
269 | const scrollHeight = | ||
270 | view.contentHeight + scrollerHeight - view.defaultLineHeight; | ||
271 | if (firstRun) { | ||
272 | if (firstRunTimeout !== undefined) { | ||
273 | clearTimeout(firstRunTimeout); | ||
274 | } | ||
275 | firstRunTimeout = setTimeout(() => { | ||
276 | spacer.style.minHeight = `${scrollHeight}px`; | ||
277 | firstRun = false; | ||
278 | }, 0); | ||
279 | } else { | ||
280 | spacer.style.minHeight = `${scrollHeight}px`; | ||
281 | } | ||
282 | gutterWidth = gutters?.clientWidth ?? 0; | ||
283 | let trackYHeight = scrollerHeight; | ||
284 | |||
285 | // Prevent spurious horizontal scrollbar by rounding up to the nearest pixel. | ||
286 | if (scrollWidth > Math.ceil(scrollerWidth)) { | ||
287 | // Leave space for horizontal scrollbar. | ||
288 | trackYHeight -= SCROLLBAR_WIDTH; | ||
289 | // Alwalys leave space for annotation in the vertical scrollbar. | ||
290 | const trackXWidth = scrollerWidth - gutterWidth - SCROLLBAR_WIDTH; | ||
291 | const thumbWidth = trackXWidth * (scrollerWidth / scrollWidth); | ||
292 | factorX = (trackXWidth - thumbWidth) / (scrollWidth - scrollerWidth); | ||
293 | trackY.style.bottom = `${SCROLLBAR_WIDTH}px`; | ||
294 | trackX.style.display = 'block'; | ||
295 | trackX.style.left = `${gutterWidth}px`; | ||
296 | thumbX.style.width = `${thumbWidth}px`; | ||
297 | thumbX.style.left = `${scrollLeft * factorX}px`; | ||
298 | scrollDOM.style.overflowX = 'scroll'; | ||
299 | } else { | ||
300 | trackY.style.bottom = '0px'; | ||
301 | trackX.style.display = 'none'; | ||
302 | scrollDOM.style.overflowX = 'hidden'; | ||
303 | } | ||
304 | |||
305 | const thumbHeight = trackYHeight * (scrollerHeight / scrollHeight); | ||
306 | factorY = (trackYHeight - thumbHeight) / (scrollHeight - scrollerHeight); | ||
307 | thumbY.style.display = 'block'; | ||
308 | thumbY.style.height = `${thumbHeight}px`; | ||
309 | thumbY.style.top = `${scrollTop * factorY}px`; | ||
310 | |||
311 | gutterDecoration.style.left = `${gutterWidth}px`; | ||
312 | gutterDecoration.style.width = `${Math.max( | ||
313 | 0, | ||
314 | Math.min(scrollLeft, SHADOW_WIDTH), | ||
315 | )}px`; | ||
316 | |||
317 | topDecoration.style.height = `${Math.max( | ||
318 | 0, | ||
319 | Math.min(scrollTop, SHADOW_WIDTH), | ||
320 | )}px`; | ||
321 | |||
322 | if (rebuildRequested) { | ||
323 | rebuildAnnotations( | ||
324 | view, | ||
325 | scrollHeight, | ||
326 | trackYHeight, | ||
327 | holder, | ||
328 | annotations, | ||
329 | ); | ||
330 | rebuildRequested = false; | ||
331 | } | ||
332 | } | ||
333 | |||
334 | function requestUpdate() { | ||
335 | if (!requested) { | ||
336 | requested = true; | ||
337 | view.requestMeasure({ read: update }); | ||
338 | } | ||
339 | } | ||
340 | |||
341 | function requestRebuild() { | ||
342 | requestUpdate(); | ||
343 | rebuildRequested = true; | ||
344 | } | ||
345 | |||
346 | observer = new ResizeObserver(requestRebuild); | ||
347 | observer.observe(holder); | ||
348 | |||
349 | scrollDOM.addEventListener('scroll', requestUpdate); | ||
350 | |||
351 | requestRebuild(); | ||
352 | |||
353 | return { | ||
354 | update: requestRebuild, | ||
355 | destroy() { | ||
356 | disposePanelReaction(); | ||
357 | observer?.disconnect(); | ||
358 | scrollDOM.removeEventListener('scroll', requestUpdate); | ||
359 | parentDOM.replaceChild(holder, holder); | ||
360 | }, | ||
361 | }; | ||
362 | }); | ||
363 | } | ||