diff options
Diffstat (limited to 'subprojects/frontend/src/editor')
-rw-r--r-- | subprojects/frontend/src/editor/EditorTheme.ts | 9 | ||||
-rw-r--r-- | subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts | 2 | ||||
-rw-r--r-- | subprojects/frontend/src/editor/scrollbarViewPlugin.ts | 71 |
3 files changed, 56 insertions, 26 deletions
diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index f5267682..c3cbffc8 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts | |||
@@ -64,6 +64,13 @@ export default styled('div', { | |||
64 | overflow: 'hidden', | 64 | overflow: 'hidden', |
65 | flex: '1 1', | 65 | flex: '1 1', |
66 | }, | 66 | }, |
67 | '.cm-scroller-spacer': { | ||
68 | position: 'sticky', | ||
69 | flexShrink: 0, | ||
70 | zIndex: 300, | ||
71 | width: 1, | ||
72 | marginRight: -1, | ||
73 | }, | ||
67 | '.cm-scroller': { | 74 | '.cm-scroller': { |
68 | color: theme.palette.text.secondary, | 75 | color: theme.palette.text.secondary, |
69 | scrollbarWidth: 'none', | 76 | scrollbarWidth: 'none', |
@@ -126,7 +133,7 @@ export default styled('div', { | |||
126 | }, | 133 | }, |
127 | '.cm-content': { | 134 | '.cm-content': { |
128 | ...editorFontStyle, | 135 | ...editorFontStyle, |
129 | padding: 0, | 136 | padding: '0 12px 0 0', |
130 | }, | 137 | }, |
131 | '.cm-activeLine': { | 138 | '.cm-activeLine': { |
132 | background: showActiveLine | 139 | background: showActiveLine |
diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts index d5ad536b..c9480c7d 100644 --- a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts +++ b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts | |||
@@ -61,7 +61,7 @@ class IndentationWidget extends WidgetType { | |||
61 | 61 | ||
62 | const wrapper = document.createElement('span'); | 62 | const wrapper = document.createElement('span'); |
63 | wrapper.style.top = '0'; | 63 | wrapper.style.top = '0'; |
64 | wrapper.style.left = '4px'; | 64 | wrapper.style.left = '6px'; |
65 | wrapper.style.position = 'absolute'; | 65 | wrapper.style.position = 'absolute'; |
66 | wrapper.style.pointerEvents = 'none'; | 66 | wrapper.style.pointerEvents = 'none'; |
67 | 67 | ||
diff --git a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts b/subprojects/frontend/src/editor/scrollbarViewPlugin.ts index b0ea769f..9ee70441 100644 --- a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts +++ b/subprojects/frontend/src/editor/scrollbarViewPlugin.ts | |||
@@ -1,3 +1,4 @@ | |||
1 | import { EditorSelection } from '@codemirror/state'; | ||
1 | import { type PluginValue, ViewPlugin } from '@codemirror/view'; | 2 | import { type PluginValue, ViewPlugin } from '@codemirror/view'; |
2 | import { reaction } from 'mobx'; | 3 | import { reaction } from 'mobx'; |
3 | 4 | ||
@@ -6,6 +7,7 @@ import { getDiagnostics } from './exposeDiagnostics'; | |||
6 | import findOccurrences from './findOccurrences'; | 7 | import findOccurrences from './findOccurrences'; |
7 | 8 | ||
8 | export const HOLDER_CLASS = 'cm-scroller-holder'; | 9 | export const HOLDER_CLASS = 'cm-scroller-holder'; |
10 | export const SPACER_CLASS = 'cm-scroller-spacer'; | ||
9 | export const THUMB_CLASS = 'cm-scroller-thumb'; | 11 | export const THUMB_CLASS = 'cm-scroller-thumb'; |
10 | export const THUMB_Y_CLASS = 'cm-scroller-thumb-y'; | 12 | export const THUMB_Y_CLASS = 'cm-scroller-thumb-y'; |
11 | export const THUMB_X_CLASS = 'cm-scroller-thumb-x'; | 13 | export const THUMB_X_CLASS = 'cm-scroller-thumb-x'; |
@@ -35,6 +37,27 @@ export default function scrollbarViewPlugin( | |||
35 | parentDOM.replaceChild(holder, scrollDOM); | 37 | parentDOM.replaceChild(holder, scrollDOM); |
36 | holder.appendChild(scrollDOM); | 38 | holder.appendChild(scrollDOM); |
37 | 39 | ||
40 | const spacer = ownerDocument.createElement('div'); | ||
41 | spacer.className = SPACER_CLASS; | ||
42 | scrollDOM.insertBefore(spacer, scrollDOM.firstChild); | ||
43 | |||
44 | let gutterWidth = 0; | ||
45 | |||
46 | scrollDOM.addEventListener('click', (event) => { | ||
47 | const scrollX = scrollDOM.scrollLeft + event.offsetX; | ||
48 | const scrollY = scrollDOM.scrollTop + event.offsetY; | ||
49 | if (scrollX > gutterWidth && scrollY > view.contentHeight) { | ||
50 | event.preventDefault(); | ||
51 | view.focus(); | ||
52 | editorStore.dispatch({ | ||
53 | scrollIntoView: true, | ||
54 | selection: EditorSelection.create([ | ||
55 | EditorSelection.cursor(view.state.doc.length), | ||
56 | ]), | ||
57 | }); | ||
58 | } | ||
59 | }); | ||
60 | |||
38 | let factorY = 1; | 61 | let factorY = 1; |
39 | let factorX = 1; | 62 | let factorX = 1; |
40 | 63 | ||
@@ -97,7 +120,6 @@ export default function scrollbarViewPlugin( | |||
97 | { fireImmediately: true }, | 120 | { fireImmediately: true }, |
98 | ); | 121 | ); |
99 | 122 | ||
100 | let observer: ResizeObserver | undefined; | ||
101 | let gutters: Element | undefined; | 123 | let gutters: Element | undefined; |
102 | 124 | ||
103 | let requested = false; | 125 | let requested = false; |
@@ -105,13 +127,11 @@ export default function scrollbarViewPlugin( | |||
105 | 127 | ||
106 | const annotations: HTMLDivElement[] = []; | 128 | const annotations: HTMLDivElement[] = []; |
107 | 129 | ||
108 | function rebuildAnnotations(trackYHeight: number) { | 130 | function rebuildAnnotations(scrollHeight: number, trackYHeight: number) { |
109 | const { state } = view; | 131 | const { state } = view; |
110 | const annotationOverlayHeight = Math.min( | 132 | const overlayAnnotationsHeight = |
111 | view.contentHeight, | 133 | (view.contentHeight / scrollHeight) * trackYHeight; |
112 | trackYHeight, | 134 | const lineHeight = overlayAnnotationsHeight / state.doc.lines; |
113 | ); | ||
114 | const lineHeight = annotationOverlayHeight / state.doc.lines; | ||
115 | 135 | ||
116 | let i = 0; | 136 | let i = 0; |
117 | 137 | ||
@@ -180,6 +200,8 @@ export default function scrollbarViewPlugin( | |||
180 | .forEach((staleAnnotation) => holder.removeChild(staleAnnotation)); | 200 | .forEach((staleAnnotation) => holder.removeChild(staleAnnotation)); |
181 | } | 201 | } |
182 | 202 | ||
203 | let observer: ResizeObserver | undefined; | ||
204 | |||
183 | function update() { | 205 | function update() { |
184 | requested = false; | 206 | requested = false; |
185 | 207 | ||
@@ -192,11 +214,15 @@ export default function scrollbarViewPlugin( | |||
192 | 214 | ||
193 | const { height: scrollerHeight, width: scrollerWidth } = | 215 | const { height: scrollerHeight, width: scrollerWidth } = |
194 | scrollDOM.getBoundingClientRect(); | 216 | scrollDOM.getBoundingClientRect(); |
195 | const { scrollTop, scrollHeight, scrollLeft, scrollWidth } = scrollDOM; | 217 | const { scrollTop, scrollLeft, scrollWidth } = scrollDOM; |
196 | const gutterWidth = gutters?.clientWidth ?? 0; | 218 | const scrollHeight = |
219 | view.contentHeight + scrollerHeight - view.defaultLineHeight; | ||
220 | spacer.style.minHeight = `${scrollHeight}px`; | ||
221 | gutterWidth = gutters?.clientWidth ?? 0; | ||
197 | let trackYHeight = scrollerHeight; | 222 | let trackYHeight = scrollerHeight; |
198 | 223 | ||
199 | if (scrollWidth > scrollerWidth) { | 224 | // Prevent spurious horizontal scrollbar by rounding up to the nearest pixel. |
225 | if (scrollWidth > Math.ceil(scrollerWidth)) { | ||
200 | // Leave space for horizontal scrollbar. | 226 | // Leave space for horizontal scrollbar. |
201 | trackYHeight -= SCROLLBAR_WIDTH; | 227 | trackYHeight -= SCROLLBAR_WIDTH; |
202 | // Alwalys leave space for annotation in the vertical scrollbar. | 228 | // Alwalys leave space for annotation in the vertical scrollbar. |
@@ -207,21 +233,18 @@ export default function scrollbarViewPlugin( | |||
207 | thumbX.style.height = `${SCROLLBAR_WIDTH}px`; | 233 | thumbX.style.height = `${SCROLLBAR_WIDTH}px`; |
208 | thumbX.style.width = `${thumbWidth}px`; | 234 | thumbX.style.width = `${thumbWidth}px`; |
209 | thumbX.style.left = `${gutterWidth + scrollLeft * factorX}px`; | 235 | thumbX.style.left = `${gutterWidth + scrollLeft * factorX}px`; |
236 | scrollDOM.style.overflowX = 'scroll'; | ||
210 | } else { | 237 | } else { |
211 | thumbX.style.display = 'none'; | 238 | thumbX.style.display = 'none'; |
239 | scrollDOM.style.overflowX = 'hidden'; | ||
212 | } | 240 | } |
213 | 241 | ||
214 | if (scrollHeight > scrollerHeight) { | 242 | const thumbHeight = trackYHeight * (scrollerHeight / scrollHeight); |
215 | const thumbHeight = trackYHeight * (scrollerHeight / scrollHeight); | 243 | factorY = (trackYHeight - thumbHeight) / (scrollHeight - scrollerHeight); |
216 | factorY = | 244 | thumbY.style.display = 'block'; |
217 | (trackYHeight - thumbHeight) / (scrollHeight - scrollerHeight); | 245 | thumbY.style.height = `${thumbHeight}px`; |
218 | thumbY.style.display = 'block'; | 246 | thumbY.style.width = `${SCROLLBAR_WIDTH}px`; |
219 | thumbY.style.height = `${thumbHeight}px`; | 247 | thumbY.style.top = `${scrollTop * factorY}px`; |
220 | thumbY.style.width = `${SCROLLBAR_WIDTH}px`; | ||
221 | thumbY.style.top = `${scrollTop * factorY}px`; | ||
222 | } else { | ||
223 | thumbY.style.display = 'none'; | ||
224 | } | ||
225 | 248 | ||
226 | gutterDecoration.style.left = `${gutterWidth}px`; | 249 | gutterDecoration.style.left = `${gutterWidth}px`; |
227 | gutterDecoration.style.width = `${Math.max( | 250 | gutterDecoration.style.width = `${Math.max( |
@@ -235,7 +258,7 @@ export default function scrollbarViewPlugin( | |||
235 | )}px`; | 258 | )}px`; |
236 | 259 | ||
237 | if (rebuildRequested) { | 260 | if (rebuildRequested) { |
238 | rebuildAnnotations(trackYHeight); | 261 | rebuildAnnotations(scrollHeight, trackYHeight); |
239 | rebuildRequested = false; | 262 | rebuildRequested = false; |
240 | } | 263 | } |
241 | } | 264 | } |
@@ -253,7 +276,7 @@ export default function scrollbarViewPlugin( | |||
253 | } | 276 | } |
254 | 277 | ||
255 | observer = new ResizeObserver(requestRebuild); | 278 | observer = new ResizeObserver(requestRebuild); |
256 | observer.observe(scrollDOM); | 279 | observer.observe(holder); |
257 | 280 | ||
258 | scrollDOM.addEventListener('scroll', requestUpdate); | 281 | scrollDOM.addEventListener('scroll', requestUpdate); |
259 | 282 | ||
@@ -265,7 +288,7 @@ export default function scrollbarViewPlugin( | |||
265 | disposePanelReaction(); | 288 | disposePanelReaction(); |
266 | observer?.disconnect(); | 289 | observer?.disconnect(); |
267 | scrollDOM.removeEventListener('scroll', requestUpdate); | 290 | scrollDOM.removeEventListener('scroll', requestUpdate); |
268 | parentDOM.replaceChild(scrollDOM, holder); | 291 | parentDOM.replaceChild(holder, holder); |
269 | }, | 292 | }, |
270 | }; | 293 | }; |
271 | }); | 294 | }); |