diff options
author | 2023-07-24 14:37:16 +0200 | |
---|---|---|
committer | 2023-07-24 14:37:16 +0200 | |
commit | 8789304690384d19ad829286560aec5ed0917976 (patch) | |
tree | b157e78e8b6a3f2fb3d0eee6e1aa10d2c16e0204 /subprojects/frontend/src/editor | |
parent | decreasing steps in fast fuzz tests (diff) | |
parent | Merge pull request #27 from kris7t/ordered-result-set (diff) | |
download | refinery-8789304690384d19ad829286560aec5ed0917976.tar.gz refinery-8789304690384d19ad829286560aec5ed0917976.tar.zst refinery-8789304690384d19ad829286560aec5ed0917976.zip |
Merge branch 'graphs4value:main' into datastructure
Diffstat (limited to 'subprojects/frontend/src/editor')
23 files changed, 129 insertions, 826 deletions
diff --git a/subprojects/frontend/src/editor/AnimatedButton.tsx b/subprojects/frontend/src/editor/AnimatedButton.tsx index f75d4617..dbbda618 100644 --- a/subprojects/frontend/src/editor/AnimatedButton.tsx +++ b/subprojects/frontend/src/editor/AnimatedButton.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import Box from '@mui/material/Box'; | 7 | import Box from '@mui/material/Box'; |
2 | import Button from '@mui/material/Button'; | 8 | import Button from '@mui/material/Button'; |
3 | import { styled, type SxProps, type Theme } from '@mui/material/styles'; | 9 | import { styled, type SxProps, type Theme } from '@mui/material/styles'; |
diff --git a/subprojects/frontend/src/editor/ConnectButton.tsx b/subprojects/frontend/src/editor/ConnectButton.tsx index e2d251f3..eed6fbc7 100644 --- a/subprojects/frontend/src/editor/ConnectButton.tsx +++ b/subprojects/frontend/src/editor/ConnectButton.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import CloudIcon from '@mui/icons-material/Cloud'; | 7 | import CloudIcon from '@mui/icons-material/Cloud'; |
2 | import CloudOffIcon from '@mui/icons-material/CloudOff'; | 8 | import CloudOffIcon from '@mui/icons-material/CloudOff'; |
3 | import SyncIcon from '@mui/icons-material/Sync'; | 9 | import SyncIcon from '@mui/icons-material/Sync'; |
diff --git a/subprojects/frontend/src/editor/ConnectionStatusNotification.tsx b/subprojects/frontend/src/editor/ConnectionStatusNotification.tsx index 9b27f45c..b7b962ab 100644 --- a/subprojects/frontend/src/editor/ConnectionStatusNotification.tsx +++ b/subprojects/frontend/src/editor/ConnectionStatusNotification.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import Button from '@mui/material/Button'; | 7 | import Button from '@mui/material/Button'; |
2 | import { observer } from 'mobx-react-lite'; | 8 | import { observer } from 'mobx-react-lite'; |
3 | import { useEffect } from 'react'; | 9 | import { useEffect } from 'react'; |
diff --git a/subprojects/frontend/src/editor/DiagnosticValue.ts b/subprojects/frontend/src/editor/DiagnosticValue.ts index b4e0b165..20478262 100644 --- a/subprojects/frontend/src/editor/DiagnosticValue.ts +++ b/subprojects/frontend/src/editor/DiagnosticValue.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import type { Diagnostic } from '@codemirror/lint'; | 7 | import type { Diagnostic } from '@codemirror/lint'; |
2 | import { RangeValue } from '@codemirror/state'; | 8 | import { RangeValue } from '@codemirror/state'; |
3 | 9 | ||
diff --git a/subprojects/frontend/src/editor/EditorArea.tsx b/subprojects/frontend/src/editor/EditorArea.tsx index cfb988b2..905fa2ec 100644 --- a/subprojects/frontend/src/editor/EditorArea.tsx +++ b/subprojects/frontend/src/editor/EditorArea.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import Box from '@mui/material/Box'; | 7 | import Box from '@mui/material/Box'; |
2 | import { useTheme } from '@mui/material/styles'; | 8 | import { useTheme } from '@mui/material/styles'; |
3 | import { observer } from 'mobx-react-lite'; | 9 | import { observer } from 'mobx-react-lite'; |
diff --git a/subprojects/frontend/src/editor/EditorButtons.tsx b/subprojects/frontend/src/editor/EditorButtons.tsx index 53b06e23..9b187e5c 100644 --- a/subprojects/frontend/src/editor/EditorButtons.tsx +++ b/subprojects/frontend/src/editor/EditorButtons.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import type { Diagnostic } from '@codemirror/lint'; | 7 | import type { Diagnostic } from '@codemirror/lint'; |
2 | import CheckIcon from '@mui/icons-material/Check'; | 8 | import CheckIcon from '@mui/icons-material/Check'; |
3 | import ErrorIcon from '@mui/icons-material/Error'; | 9 | import ErrorIcon from '@mui/icons-material/Error'; |
diff --git a/subprojects/frontend/src/editor/EditorPane.tsx b/subprojects/frontend/src/editor/EditorPane.tsx index f7f8241a..87f408fe 100644 --- a/subprojects/frontend/src/editor/EditorPane.tsx +++ b/subprojects/frontend/src/editor/EditorPane.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import Box from '@mui/material/Box'; | 7 | import Box from '@mui/material/Box'; |
2 | import Skeleton from '@mui/material/Skeleton'; | 8 | import Skeleton from '@mui/material/Skeleton'; |
3 | import Stack from '@mui/material/Stack'; | 9 | import Stack from '@mui/material/Stack'; |
diff --git a/subprojects/frontend/src/editor/EditorStore.ts b/subprojects/frontend/src/editor/EditorStore.ts index 0a0d885d..b98f085e 100644 --- a/subprojects/frontend/src/editor/EditorStore.ts +++ b/subprojects/frontend/src/editor/EditorStore.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import type { | 7 | import type { |
2 | CompletionContext, | 8 | CompletionContext, |
3 | CompletionResult, | 9 | CompletionResult, |
diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts index 01b65a7e..e057ce18 100644 --- a/subprojects/frontend/src/editor/EditorTheme.ts +++ b/subprojects/frontend/src/editor/EditorTheme.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import errorSVG from '@material-icons/svg/svg/error/baseline.svg?raw'; | 7 | import errorSVG from '@material-icons/svg/svg/error/baseline.svg?raw'; |
2 | import expandMoreSVG from '@material-icons/svg/svg/expand_more/baseline.svg?raw'; | 8 | import expandMoreSVG from '@material-icons/svg/svg/expand_more/baseline.svg?raw'; |
3 | import infoSVG from '@material-icons/svg/svg/info/baseline.svg?raw'; | 9 | import infoSVG from '@material-icons/svg/svg/info/baseline.svg?raw'; |
@@ -8,32 +14,6 @@ function svgURL(svg: string): string { | |||
8 | return `url('data:image/svg+xml;utf8,${svg}')`; | 14 | return `url('data:image/svg+xml;utf8,${svg}')`; |
9 | } | 15 | } |
10 | 16 | ||
11 | function radialShadowTheme( | ||
12 | origin: string, | ||
13 | scaleX: boolean, | ||
14 | scaleY: boolean, | ||
15 | ): CSSObject { | ||
16 | function radialGradient(opacity: number, scale: string): string { | ||
17 | return `radial-gradient( | ||
18 | farthest-side at ${origin}, | ||
19 | rgba(0, 0, 0, ${opacity}), | ||
20 | rgba(0, 0, 0, 0) | ||
21 | ) | ||
22 | ${origin} / | ||
23 | ${scaleX ? scale : '100%'} | ||
24 | ${scaleY ? scale : '100%'} | ||
25 | no-repeat`; | ||
26 | } | ||
27 | |||
28 | return { | ||
29 | background: ` | ||
30 | ${radialGradient(0.2, '40%')}, | ||
31 | ${radialGradient(0.14, '50%')}, | ||
32 | ${radialGradient(0.12, '100%')} | ||
33 | `, | ||
34 | }; | ||
35 | } | ||
36 | |||
37 | export default styled('div', { | 17 | export default styled('div', { |
38 | name: 'EditorTheme', | 18 | name: 'EditorTheme', |
39 | shouldForwardProp: (propName) => | 19 | shouldForwardProp: (propName) => |
@@ -52,98 +32,13 @@ export default styled('div', { | |||
52 | }, | 32 | }, |
53 | }; | 33 | }; |
54 | 34 | ||
55 | const scrollerThumbOpacity = theme.palette.mode === 'dark' ? 0.16 : 0.28; | ||
56 | |||
57 | const generalStyle: CSSObject = { | 35 | const generalStyle: CSSObject = { |
58 | background: theme.palette.background.default, | 36 | background: theme.palette.background.default, |
59 | '&, .cm-editor': { | 37 | '&, .cm-editor': { |
60 | height: '100%', | 38 | height: '100%', |
61 | }, | 39 | }, |
62 | '.cm-scroller-holder': { | ||
63 | display: 'flex', | ||
64 | position: 'relative', | ||
65 | flexDirection: 'column', | ||
66 | overflow: 'hidden', | ||
67 | flex: '1 1', | ||
68 | }, | ||
69 | '.cm-scroller-spacer': { | ||
70 | position: 'sticky', | ||
71 | flexShrink: 0, | ||
72 | zIndex: 300, | ||
73 | width: 1, | ||
74 | marginRight: -1, | ||
75 | pointerEvents: 'none', | ||
76 | }, | ||
77 | '.cm-scroller': { | 40 | '.cm-scroller': { |
78 | color: theme.palette.text.secondary, | 41 | color: theme.palette.text.secondary, |
79 | scrollbarWidth: 'none', | ||
80 | MsOverflowStyle: 'none', | ||
81 | '&::-webkit-scrollbar': { | ||
82 | width: 0, | ||
83 | height: 0, | ||
84 | background: 'transparent', | ||
85 | }, | ||
86 | }, | ||
87 | '.cm-scroller-track': { | ||
88 | position: 'absolute', | ||
89 | zIndex: 300, | ||
90 | touchAction: 'none', | ||
91 | }, | ||
92 | '.cm-scroller-thumb': { | ||
93 | position: 'absolute', | ||
94 | background: theme.palette.text.secondary, | ||
95 | opacity: scrollerThumbOpacity, | ||
96 | transition: theme.transitions.create('opacity', { | ||
97 | duration: theme.transitions.duration.shortest, | ||
98 | }), | ||
99 | touchAction: 'none', | ||
100 | WebkitTapHighlightColor: 'transparent', | ||
101 | '&:hover': { | ||
102 | opacity: 0.75, | ||
103 | '@media (hover: none)': { | ||
104 | opacity: scrollerThumbOpacity, | ||
105 | }, | ||
106 | }, | ||
107 | '&.active': { | ||
108 | opacity: 1, | ||
109 | pointerEvents: 'none', | ||
110 | userSelect: 'none', | ||
111 | }, | ||
112 | }, | ||
113 | '.cm-scroller-track-y, .cm-scroller-thumb-y': { | ||
114 | top: 0, | ||
115 | right: 0, | ||
116 | width: 12, | ||
117 | }, | ||
118 | '.cm-scroller-track-x, .cm-scroller-thumb-x': { | ||
119 | left: 0, | ||
120 | bottom: 0, | ||
121 | height: 12, | ||
122 | }, | ||
123 | '.cm-scroller-track-x': { | ||
124 | right: 12, | ||
125 | }, | ||
126 | '.cm-scroller-gutter-decoration': { | ||
127 | position: 'absolute', | ||
128 | top: 0, | ||
129 | bottom: 0, | ||
130 | left: 0, | ||
131 | width: 0, | ||
132 | transition: theme.transitions.create('width', { | ||
133 | duration: theme.transitions.duration.shortest, | ||
134 | }), | ||
135 | ...radialShadowTheme('0 50%', true, false), | ||
136 | }, | ||
137 | '.cm-scroller-top-decoration': { | ||
138 | position: 'absolute', | ||
139 | top: 0, | ||
140 | left: 0, | ||
141 | right: 0, | ||
142 | height: 0, | ||
143 | transition: theme.transitions.create('height', { | ||
144 | duration: theme.transitions.duration.shortest, | ||
145 | }), | ||
146 | ...radialShadowTheme('50% 0', false, true), | ||
147 | }, | 42 | }, |
148 | '.cm-gutters': { | 43 | '.cm-gutters': { |
149 | background: theme.palette.background.default, | 44 | background: theme.palette.background.default, |
@@ -162,7 +57,6 @@ export default styled('div', { | |||
162 | background: 'transparent', | 57 | background: 'transparent', |
163 | }, | 58 | }, |
164 | '.cm-cursor, .cm-cursor-primary': { | 59 | '.cm-cursor, .cm-cursor-primary': { |
165 | marginLeft: -1, | ||
166 | borderLeft: `2px solid ${theme.palette.info.main}`, | 60 | borderLeft: `2px solid ${theme.palette.info.main}`, |
167 | }, | 61 | }, |
168 | '.cm-selectionBackground': { | 62 | '.cm-selectionBackground': { |
@@ -175,7 +69,6 @@ export default styled('div', { | |||
175 | }, | 69 | }, |
176 | }, | 70 | }, |
177 | '.cm-line': { | 71 | '.cm-line': { |
178 | position: 'relative', // For indentation highlights | ||
179 | padding: '0 12px 0 0px', | 72 | padding: '0 12px 0 0px', |
180 | }, | 73 | }, |
181 | }; | 74 | }; |
@@ -265,13 +158,6 @@ export default styled('div', { | |||
265 | '.cm-searchMatch-selected': { | 158 | '.cm-searchMatch-selected': { |
266 | background: theme.palette.highlight.search.selected, | 159 | background: theme.palette.highlight.search.selected, |
267 | }, | 160 | }, |
268 | '.cm-indentation-marker': { | ||
269 | display: 'inline-block', | ||
270 | boxShadow: `1px 0 0 ${theme.palette.text.disabled} inset`, | ||
271 | '&.active': { | ||
272 | boxShadow: `1px 0 0 ${theme.palette.text.primary} inset`, | ||
273 | }, | ||
274 | }, | ||
275 | '.cm-scroller-selection': { | 161 | '.cm-scroller-selection': { |
276 | position: 'absolute', | 162 | position: 'absolute', |
277 | right: 0, | 163 | right: 0, |
@@ -452,11 +338,11 @@ export default styled('div', { | |||
452 | 338 | ||
453 | const foldStyle = { | 339 | const foldStyle = { |
454 | '.cm-foldGutter': { | 340 | '.cm-foldGutter': { |
455 | width: 17, | 341 | width: 16, |
456 | }, | 342 | }, |
457 | '.problem-editor-foldMarker': { | 343 | '.problem-editor-foldMarker': { |
458 | display: 'block', | 344 | display: 'block', |
459 | margin: '4px 1px 4px 0', | 345 | margin: '4px 0 4px 0', |
460 | padding: 0, | 346 | padding: 0, |
461 | maskImage: svgURL(expandMoreSVG), | 347 | maskImage: svgURL(expandMoreSVG), |
462 | maskSize: '16px 16px', | 348 | maskSize: '16px 16px', |
@@ -467,7 +353,7 @@ export default styled('div', { | |||
467 | cursor: 'pointer', | 353 | cursor: 'pointer', |
468 | WebkitTapHighlightColor: 'transparent', | 354 | WebkitTapHighlightColor: 'transparent', |
469 | [theme.breakpoints.down('sm')]: { | 355 | [theme.breakpoints.down('sm')]: { |
470 | margin: '2px 1px 2px 0', | 356 | margin: '2px 0 2px 0', |
471 | }, | 357 | }, |
472 | }, | 358 | }, |
473 | '.problem-editor-foldMarker-open': { | 359 | '.problem-editor-foldMarker-open': { |
diff --git a/subprojects/frontend/src/editor/GenerateButton.tsx b/subprojects/frontend/src/editor/GenerateButton.tsx index 2036fc28..3837ef8e 100644 --- a/subprojects/frontend/src/editor/GenerateButton.tsx +++ b/subprojects/frontend/src/editor/GenerateButton.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import DangerousOutlinedIcon from '@mui/icons-material/DangerousOutlined'; | 7 | import DangerousOutlinedIcon from '@mui/icons-material/DangerousOutlined'; |
2 | import PlayArrowIcon from '@mui/icons-material/PlayArrow'; | 8 | import PlayArrowIcon from '@mui/icons-material/PlayArrow'; |
3 | import Button from '@mui/material/Button'; | 9 | import Button from '@mui/material/Button'; |
diff --git a/subprojects/frontend/src/editor/LintPanelStore.ts b/subprojects/frontend/src/editor/LintPanelStore.ts index 502f9c59..f81587fa 100644 --- a/subprojects/frontend/src/editor/LintPanelStore.ts +++ b/subprojects/frontend/src/editor/LintPanelStore.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { closeLintPanel, openLintPanel } from '@codemirror/lint'; | 7 | import { closeLintPanel, openLintPanel } from '@codemirror/lint'; |
2 | 8 | ||
3 | import type EditorStore from './EditorStore'; | 9 | import type EditorStore from './EditorStore'; |
diff --git a/subprojects/frontend/src/editor/PanelStore.ts b/subprojects/frontend/src/editor/PanelStore.ts index 4f827280..25ef8b6c 100644 --- a/subprojects/frontend/src/editor/PanelStore.ts +++ b/subprojects/frontend/src/editor/PanelStore.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import type { Command } from '@codemirror/view'; | 7 | import type { Command } from '@codemirror/view'; |
2 | import { action, makeObservable, observable } from 'mobx'; | 8 | import { action, makeObservable, observable } from 'mobx'; |
3 | 9 | ||
diff --git a/subprojects/frontend/src/editor/SearchPanel.ts b/subprojects/frontend/src/editor/SearchPanel.ts index c9df41b7..b63d5eed 100644 --- a/subprojects/frontend/src/editor/SearchPanel.ts +++ b/subprojects/frontend/src/editor/SearchPanel.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { | 7 | import { |
2 | type EditorView, | 8 | type EditorView, |
3 | type Panel, | 9 | type Panel, |
diff --git a/subprojects/frontend/src/editor/SearchPanelPortal.tsx b/subprojects/frontend/src/editor/SearchPanelPortal.tsx index 5cf1c90e..b4b07c74 100644 --- a/subprojects/frontend/src/editor/SearchPanelPortal.tsx +++ b/subprojects/frontend/src/editor/SearchPanelPortal.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import Portal from '@mui/material/Portal'; | 7 | import Portal from '@mui/material/Portal'; |
2 | import { observer } from 'mobx-react-lite'; | 8 | import { observer } from 'mobx-react-lite'; |
3 | 9 | ||
diff --git a/subprojects/frontend/src/editor/SearchPanelStore.ts b/subprojects/frontend/src/editor/SearchPanelStore.ts index 65d595a8..6a97baf1 100644 --- a/subprojects/frontend/src/editor/SearchPanelStore.ts +++ b/subprojects/frontend/src/editor/SearchPanelStore.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { | 7 | import { |
2 | closeSearchPanel, | 8 | closeSearchPanel, |
3 | findNext, | 9 | findNext, |
diff --git a/subprojects/frontend/src/editor/SearchToolbar.tsx b/subprojects/frontend/src/editor/SearchToolbar.tsx index 54f3dba7..4ae7e893 100644 --- a/subprojects/frontend/src/editor/SearchToolbar.tsx +++ b/subprojects/frontend/src/editor/SearchToolbar.tsx | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import CloseIcon from '@mui/icons-material/Close'; | 7 | import CloseIcon from '@mui/icons-material/Close'; |
2 | import FindReplaceIcon from '@mui/icons-material/FindReplace'; | 8 | import FindReplaceIcon from '@mui/icons-material/FindReplace'; |
3 | import KeyboardArrowDownIcon from '@mui/icons-material/KeyboardArrowDown'; | 9 | import KeyboardArrowDownIcon from '@mui/icons-material/KeyboardArrowDown'; |
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts index ce1efa4f..67b8fb9e 100644 --- a/subprojects/frontend/src/editor/createEditorState.ts +++ b/subprojects/frontend/src/editor/createEditorState.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { | 7 | import { |
2 | closeBrackets, | 8 | closeBrackets, |
3 | closeBracketsKeymap, | 9 | closeBracketsKeymap, |
@@ -38,8 +44,6 @@ import type EditorStore from './EditorStore'; | |||
38 | import SearchPanel from './SearchPanel'; | 44 | import SearchPanel from './SearchPanel'; |
39 | import exposeDiagnostics from './exposeDiagnostics'; | 45 | import exposeDiagnostics from './exposeDiagnostics'; |
40 | import findOccurrences from './findOccurrences'; | 46 | import findOccurrences from './findOccurrences'; |
41 | import indentationMarkerViewPlugin from './indentationMarkerViewPlugin'; | ||
42 | import scrollbarViewPlugin from './scrollbarViewPlugin'; | ||
43 | import semanticHighlighting from './semanticHighlighting'; | 47 | import semanticHighlighting from './semanticHighlighting'; |
44 | 48 | ||
45 | export default function createEditorState( | 49 | export default function createEditorState( |
@@ -64,7 +68,6 @@ export default function createEditorState( | |||
64 | highlightSpecialChars(), | 68 | highlightSpecialChars(), |
65 | history(), | 69 | history(), |
66 | indentOnInput(), | 70 | indentOnInput(), |
67 | indentationMarkerViewPlugin(), | ||
68 | rectangularSelection(), | 71 | rectangularSelection(), |
69 | search({ | 72 | search({ |
70 | createPanel(view) { | 73 | createPanel(view) { |
@@ -123,7 +126,6 @@ export default function createEditorState( | |||
123 | ...defaultKeymap, | 126 | ...defaultKeymap, |
124 | ]), | 127 | ]), |
125 | problemLanguageSupport(), | 128 | problemLanguageSupport(), |
126 | scrollbarViewPlugin(store), | ||
127 | ], | 129 | ], |
128 | }); | 130 | }); |
129 | } | 131 | } |
diff --git a/subprojects/frontend/src/editor/defineDecorationSetExtension.ts b/subprojects/frontend/src/editor/defineDecorationSetExtension.ts index d9c7bc7d..0887c92e 100644 --- a/subprojects/frontend/src/editor/defineDecorationSetExtension.ts +++ b/subprojects/frontend/src/editor/defineDecorationSetExtension.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { StateEffect, StateField, TransactionSpec } from '@codemirror/state'; | 7 | import { StateEffect, StateField, TransactionSpec } from '@codemirror/state'; |
2 | import { EditorView, Decoration, DecorationSet } from '@codemirror/view'; | 8 | import { EditorView, Decoration, DecorationSet } from '@codemirror/view'; |
3 | 9 | ||
diff --git a/subprojects/frontend/src/editor/exposeDiagnostics.ts b/subprojects/frontend/src/editor/exposeDiagnostics.ts index 82f24c93..c4dcbb87 100644 --- a/subprojects/frontend/src/editor/exposeDiagnostics.ts +++ b/subprojects/frontend/src/editor/exposeDiagnostics.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { setDiagnosticsEffect } from '@codemirror/lint'; | 7 | import { setDiagnosticsEffect } from '@codemirror/lint'; |
2 | import { | 8 | import { |
3 | StateField, | 9 | StateField, |
diff --git a/subprojects/frontend/src/editor/findOccurrences.ts b/subprojects/frontend/src/editor/findOccurrences.ts index 08c078c2..00dffc96 100644 --- a/subprojects/frontend/src/editor/findOccurrences.ts +++ b/subprojects/frontend/src/editor/findOccurrences.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { | 7 | import { |
2 | type Range, | 8 | type Range, |
3 | RangeSet, | 9 | RangeSet, |
diff --git a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts b/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts deleted file mode 100644 index 730fa6e3..00000000 --- a/subprojects/frontend/src/editor/indentationMarkerViewPlugin.ts +++ /dev/null | |||
@@ -1,341 +0,0 @@ | |||
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 = '0'; | ||
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 | undefined; | ||
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 | } | ||
diff --git a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts b/subprojects/frontend/src/editor/scrollbarViewPlugin.ts deleted file mode 100644 index f54251a9..00000000 --- a/subprojects/frontend/src/editor/scrollbarViewPlugin.ts +++ /dev/null | |||
@@ -1,358 +0,0 @@ | |||
1 | import { EditorSelection } from '@codemirror/state'; | ||
2 | import { | ||
3 | type EditorView, | ||
4 | type PluginValue, | ||
5 | ViewPlugin, | ||
6 | } from '@codemirror/view'; | ||
7 | import { reaction } from 'mobx'; | ||
8 | |||
9 | import type EditorStore from './EditorStore'; | ||
10 | import { getDiagnostics } from './exposeDiagnostics'; | ||
11 | import findOccurrences from './findOccurrences'; | ||
12 | |||
13 | export const HOLDER_CLASS = 'cm-scroller-holder'; | ||
14 | export const SPACER_CLASS = 'cm-scroller-spacer'; | ||
15 | export const TRACK_CLASS = 'cm-scroller-track'; | ||
16 | export const THUMB_CLASS = 'cm-scroller-thumb'; | ||
17 | export const THUMB_ACTIVE_CLASS = 'active'; | ||
18 | export const GUTTER_DECORATION_CLASS = 'cm-scroller-gutter-decoration'; | ||
19 | export const TOP_DECORATION_CLASS = 'cm-scroller-top-decoration'; | ||
20 | export const ANNOTATION_SELECTION_CLASS = 'cm-scroller-selection'; | ||
21 | export const ANNOTATION_DIAGNOSTIC_CLASS = 'cm-scroller-diagnostic'; | ||
22 | export const ANNOTATION_OCCURRENCE_CLASS = 'cm-scroller-occurrence'; | ||
23 | export const SHADOW_WIDTH = 10; | ||
24 | export const SCROLLBAR_WIDTH = 12; | ||
25 | export const ANNOTATION_WIDTH = SCROLLBAR_WIDTH / 2; | ||
26 | export const MIN_ANNOTATION_HEIGHT = 1; | ||
27 | |||
28 | function createScrollbar( | ||
29 | holder: HTMLElement, | ||
30 | direction: 'x' | 'y', | ||
31 | touchCallback: (offsetX: number, offsetY: number) => void, | ||
32 | moveCallback: (movementX: number, movementY: number) => void, | ||
33 | ): { track: HTMLElement; thumb: HTMLElement } { | ||
34 | const track = holder.ownerDocument.createElement('div'); | ||
35 | track.className = `${TRACK_CLASS} ${TRACK_CLASS}-${direction}`; | ||
36 | holder.appendChild(track); | ||
37 | |||
38 | const thumb = holder.ownerDocument.createElement('div'); | ||
39 | thumb.className = `${THUMB_CLASS} ${THUMB_CLASS}-${direction}`; | ||
40 | track.appendChild(thumb); | ||
41 | |||
42 | let pointerId: number | undefined; | ||
43 | track.addEventListener('pointerdown', (event) => { | ||
44 | if (pointerId !== undefined) { | ||
45 | event.preventDefault(); | ||
46 | return; | ||
47 | } | ||
48 | ({ pointerId } = event); | ||
49 | thumb.classList.add(THUMB_ACTIVE_CLASS); | ||
50 | if (event.target === thumb) { | ||
51 | // Prevent implicit pointer capture on mobile. | ||
52 | thumb.releasePointerCapture(pointerId); | ||
53 | } else { | ||
54 | touchCallback(event.offsetX, event.offsetY); | ||
55 | } | ||
56 | track.setPointerCapture(pointerId); | ||
57 | }); | ||
58 | |||
59 | track.addEventListener('pointermove', (event) => { | ||
60 | if (event.pointerId !== pointerId) { | ||
61 | return; | ||
62 | } | ||
63 | moveCallback(event.movementX, event.movementY); | ||
64 | event.preventDefault(); | ||
65 | }); | ||
66 | |||
67 | function scrollEnd(event: PointerEvent) { | ||
68 | if (event.pointerId !== pointerId) { | ||
69 | return; | ||
70 | } | ||
71 | pointerId = undefined; | ||
72 | thumb.classList.remove(THUMB_ACTIVE_CLASS); | ||
73 | } | ||
74 | |||
75 | track.addEventListener('pointerup', scrollEnd, { passive: true }); | ||
76 | track.addEventListener('pointercancel', scrollEnd, { passive: true }); | ||
77 | |||
78 | return { track, thumb }; | ||
79 | } | ||
80 | |||
81 | function rebuildAnnotations( | ||
82 | view: EditorView, | ||
83 | scrollHeight: number, | ||
84 | trackYHeight: number, | ||
85 | holder: HTMLElement, | ||
86 | annotations: HTMLDivElement[], | ||
87 | ) { | ||
88 | const { state } = view; | ||
89 | const overlayAnnotationsHeight = | ||
90 | (view.contentHeight / scrollHeight) * trackYHeight; | ||
91 | const lineHeight = overlayAnnotationsHeight / state.doc.lines; | ||
92 | |||
93 | let i = 0; | ||
94 | |||
95 | function getOrCreateAnnotation(from: number, to?: number): HTMLDivElement { | ||
96 | const startLine = state.doc.lineAt(from).number; | ||
97 | const endLine = to === undefined ? startLine : state.doc.lineAt(to).number; | ||
98 | const top = (startLine - 1) * lineHeight; | ||
99 | const height = Math.max( | ||
100 | MIN_ANNOTATION_HEIGHT, | ||
101 | Math.max(1, endLine - startLine) * lineHeight, | ||
102 | ); | ||
103 | |||
104 | let annotation: HTMLDivElement | undefined; | ||
105 | if (i < annotations.length) { | ||
106 | annotation = annotations[i]; | ||
107 | } | ||
108 | if (annotation === undefined) { | ||
109 | annotation = holder.ownerDocument.createElement('div'); | ||
110 | annotations.push(annotation); | ||
111 | holder.appendChild(annotation); | ||
112 | } | ||
113 | i += 1; | ||
114 | |||
115 | annotation.style.top = `${top}px`; | ||
116 | annotation.style.height = `${height}px`; | ||
117 | |||
118 | return annotation; | ||
119 | } | ||
120 | |||
121 | state.selection.ranges.forEach(({ head }) => { | ||
122 | const selectionAnnotation = getOrCreateAnnotation(head); | ||
123 | selectionAnnotation.className = ANNOTATION_SELECTION_CLASS; | ||
124 | selectionAnnotation.style.width = `${SCROLLBAR_WIDTH}px`; | ||
125 | }); | ||
126 | |||
127 | const diagnosticsIter = getDiagnostics(state).iter(); | ||
128 | while (diagnosticsIter.value !== null) { | ||
129 | const diagnosticAnnotation = getOrCreateAnnotation( | ||
130 | diagnosticsIter.from, | ||
131 | diagnosticsIter.to, | ||
132 | ); | ||
133 | diagnosticAnnotation.className = `${ANNOTATION_DIAGNOSTIC_CLASS} ${ANNOTATION_DIAGNOSTIC_CLASS}-${diagnosticsIter.value.severity}`; | ||
134 | diagnosticAnnotation.style.width = `${ANNOTATION_WIDTH}px`; | ||
135 | diagnosticsIter.next(); | ||
136 | } | ||
137 | |||
138 | const occurrences = view.state.field(findOccurrences); | ||
139 | const occurrencesIter = occurrences.iter(); | ||
140 | while (occurrencesIter.value !== null) { | ||
141 | const occurrenceAnnotation = getOrCreateAnnotation( | ||
142 | occurrencesIter.from, | ||
143 | occurrencesIter.to, | ||
144 | ); | ||
145 | occurrenceAnnotation.className = ANNOTATION_OCCURRENCE_CLASS; | ||
146 | occurrenceAnnotation.style.width = `${ANNOTATION_WIDTH}px`; | ||
147 | occurrenceAnnotation.style.right = `${ANNOTATION_WIDTH}px`; | ||
148 | occurrencesIter.next(); | ||
149 | } | ||
150 | |||
151 | annotations | ||
152 | .splice(i) | ||
153 | .forEach((staleAnnotation) => holder.removeChild(staleAnnotation)); | ||
154 | } | ||
155 | |||
156 | export default function scrollbarViewPlugin( | ||
157 | editorStore: EditorStore, | ||
158 | ): ViewPlugin<PluginValue> { | ||
159 | return ViewPlugin.define((view) => { | ||
160 | const { scrollDOM } = view; | ||
161 | const { ownerDocument, parentElement: parentDOM } = scrollDOM; | ||
162 | if (parentDOM === null) { | ||
163 | return {}; | ||
164 | } | ||
165 | |||
166 | const holder = ownerDocument.createElement('div'); | ||
167 | holder.className = HOLDER_CLASS; | ||
168 | parentDOM.replaceChild(holder, scrollDOM); | ||
169 | holder.appendChild(scrollDOM); | ||
170 | |||
171 | const spacer = ownerDocument.createElement('div'); | ||
172 | spacer.className = SPACER_CLASS; | ||
173 | scrollDOM.insertBefore(spacer, scrollDOM.firstChild); | ||
174 | |||
175 | let gutterWidth = 0; | ||
176 | |||
177 | scrollDOM.addEventListener('click', (event) => { | ||
178 | const scrollX = scrollDOM.scrollLeft + event.offsetX; | ||
179 | const scrollY = scrollDOM.scrollTop + event.offsetY; | ||
180 | if (scrollX > gutterWidth && scrollY > view.contentHeight) { | ||
181 | event.preventDefault(); | ||
182 | view.focus(); | ||
183 | editorStore.dispatch({ | ||
184 | scrollIntoView: true, | ||
185 | selection: EditorSelection.create([ | ||
186 | EditorSelection.cursor(view.state.doc.length), | ||
187 | ]), | ||
188 | }); | ||
189 | } | ||
190 | }); | ||
191 | |||
192 | let factorY = 1; | ||
193 | let factorX = 1; | ||
194 | |||
195 | const { track: trackY, thumb: thumbY } = createScrollbar( | ||
196 | holder, | ||
197 | 'y', | ||
198 | (_offsetX, offsetY) => { | ||
199 | const scaledOffset = offsetY / factorY; | ||
200 | const { height: scrollerHeight } = scrollDOM.getBoundingClientRect(); | ||
201 | const target = Math.max(0, scaledOffset - scrollerHeight / 2); | ||
202 | scrollDOM.scrollTo({ top: target }); | ||
203 | }, | ||
204 | (_movementX, movementY) => { | ||
205 | scrollDOM.scrollBy({ top: movementY / factorY }); | ||
206 | }, | ||
207 | ); | ||
208 | |||
209 | const { track: trackX, thumb: thumbX } = createScrollbar( | ||
210 | holder, | ||
211 | 'x', | ||
212 | (offsetX) => { | ||
213 | const scaledOffset = offsetX / factorX; | ||
214 | const { width: scrollerWidth } = scrollDOM.getBoundingClientRect(); | ||
215 | const target = Math.max(0, scaledOffset - scrollerWidth / 2); | ||
216 | scrollDOM.scrollTo({ left: target }); | ||
217 | }, | ||
218 | (movementX) => { | ||
219 | scrollDOM.scrollBy({ left: movementX / factorX }); | ||
220 | }, | ||
221 | ); | ||
222 | |||
223 | const gutterDecoration = ownerDocument.createElement('div'); | ||
224 | gutterDecoration.className = GUTTER_DECORATION_CLASS; | ||
225 | holder.appendChild(gutterDecoration); | ||
226 | |||
227 | const topDecoration = ownerDocument.createElement('div'); | ||
228 | topDecoration.className = TOP_DECORATION_CLASS; | ||
229 | holder.appendChild(topDecoration); | ||
230 | |||
231 | const disposePanelReaction = reaction( | ||
232 | () => editorStore.searchPanel.state, | ||
233 | (panelOpen) => { | ||
234 | topDecoration.style.display = panelOpen ? 'none' : 'block'; | ||
235 | }, | ||
236 | { fireImmediately: true }, | ||
237 | ); | ||
238 | |||
239 | let gutters: Element | undefined; | ||
240 | |||
241 | let firstRun = true; | ||
242 | let firstRunTimeout: number | undefined; | ||
243 | let requested = false; | ||
244 | let rebuildRequested = false; | ||
245 | |||
246 | const annotations: HTMLDivElement[] = []; | ||
247 | |||
248 | let observer: ResizeObserver | undefined; | ||
249 | |||
250 | function update() { | ||
251 | requested = false; | ||
252 | |||
253 | if (gutters === undefined) { | ||
254 | gutters = scrollDOM.querySelector('.cm-gutters') ?? undefined; | ||
255 | if (gutters !== undefined && observer !== undefined) { | ||
256 | observer.observe(gutters); | ||
257 | } | ||
258 | } | ||
259 | |||
260 | const { height: scrollerHeight, width: scrollerWidth } = | ||
261 | scrollDOM.getBoundingClientRect(); | ||
262 | const { scrollTop, scrollLeft, scrollWidth } = scrollDOM; | ||
263 | const scrollHeight = | ||
264 | view.contentHeight + scrollerHeight - view.defaultLineHeight; | ||
265 | if (firstRun) { | ||
266 | if (firstRunTimeout !== undefined) { | ||
267 | clearTimeout(firstRunTimeout); | ||
268 | } | ||
269 | // @ts-expect-error `@types/node` typings should not be in effect here. | ||
270 | firstRunTimeout = setTimeout(() => { | ||
271 | spacer.style.minHeight = `${scrollHeight}px`; | ||
272 | firstRun = false; | ||
273 | }, 0); | ||
274 | } else { | ||
275 | spacer.style.minHeight = `${scrollHeight}px`; | ||
276 | } | ||
277 | gutterWidth = gutters?.clientWidth ?? 0; | ||
278 | let trackYHeight = scrollerHeight; | ||
279 | |||
280 | // Prevent spurious horizontal scrollbar by rounding up to the nearest pixel. | ||
281 | if (scrollWidth > Math.ceil(scrollerWidth)) { | ||
282 | // Leave space for horizontal scrollbar. | ||
283 | trackYHeight -= SCROLLBAR_WIDTH; | ||
284 | // Alwalys leave space for annotation in the vertical scrollbar. | ||
285 | const trackXWidth = scrollerWidth - gutterWidth - SCROLLBAR_WIDTH; | ||
286 | const thumbWidth = trackXWidth * (scrollerWidth / scrollWidth); | ||
287 | factorX = (trackXWidth - thumbWidth) / (scrollWidth - scrollerWidth); | ||
288 | trackY.style.bottom = `${SCROLLBAR_WIDTH}px`; | ||
289 | trackX.style.display = 'block'; | ||
290 | trackX.style.left = `${gutterWidth}px`; | ||
291 | thumbX.style.width = `${thumbWidth}px`; | ||
292 | thumbX.style.left = `${scrollLeft * factorX}px`; | ||
293 | scrollDOM.style.overflowX = 'scroll'; | ||
294 | } else { | ||
295 | trackY.style.bottom = '0px'; | ||
296 | trackX.style.display = 'none'; | ||
297 | scrollDOM.style.overflowX = 'hidden'; | ||
298 | } | ||
299 | |||
300 | const thumbHeight = trackYHeight * (scrollerHeight / scrollHeight); | ||
301 | factorY = (trackYHeight - thumbHeight) / (scrollHeight - scrollerHeight); | ||
302 | thumbY.style.display = 'block'; | ||
303 | thumbY.style.height = `${thumbHeight}px`; | ||
304 | thumbY.style.top = `${scrollTop * factorY}px`; | ||
305 | |||
306 | gutterDecoration.style.left = `${gutterWidth}px`; | ||
307 | gutterDecoration.style.width = `${Math.max( | ||
308 | 0, | ||
309 | Math.min(scrollLeft, SHADOW_WIDTH), | ||
310 | )}px`; | ||
311 | |||
312 | topDecoration.style.height = `${Math.max( | ||
313 | 0, | ||
314 | Math.min(scrollTop, SHADOW_WIDTH), | ||
315 | )}px`; | ||
316 | |||
317 | if (rebuildRequested) { | ||
318 | rebuildAnnotations( | ||
319 | view, | ||
320 | scrollHeight, | ||
321 | trackYHeight, | ||
322 | holder, | ||
323 | annotations, | ||
324 | ); | ||
325 | rebuildRequested = false; | ||
326 | } | ||
327 | } | ||
328 | |||
329 | function requestUpdate() { | ||
330 | if (!requested) { | ||
331 | requested = true; | ||
332 | view.requestMeasure({ read: update }); | ||
333 | } | ||
334 | } | ||
335 | |||
336 | function requestRebuild() { | ||
337 | requestUpdate(); | ||
338 | rebuildRequested = true; | ||
339 | } | ||
340 | |||
341 | observer = new ResizeObserver(requestRebuild); | ||
342 | observer.observe(holder); | ||
343 | |||
344 | scrollDOM.addEventListener('scroll', requestUpdate); | ||
345 | |||
346 | requestRebuild(); | ||
347 | |||
348 | return { | ||
349 | update: requestRebuild, | ||
350 | destroy() { | ||
351 | disposePanelReaction(); | ||
352 | observer?.disconnect(); | ||
353 | scrollDOM.removeEventListener('scroll', requestUpdate); | ||
354 | parentDOM.replaceChild(holder, holder); | ||
355 | }, | ||
356 | }; | ||
357 | }); | ||
358 | } | ||
diff --git a/subprojects/frontend/src/editor/semanticHighlighting.ts b/subprojects/frontend/src/editor/semanticHighlighting.ts index 2c1bd67d..1f2e564c 100644 --- a/subprojects/frontend/src/editor/semanticHighlighting.ts +++ b/subprojects/frontend/src/editor/semanticHighlighting.ts | |||
@@ -1,3 +1,9 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | |||
1 | import { RangeSet, type TransactionSpec } from '@codemirror/state'; | 7 | import { RangeSet, type TransactionSpec } from '@codemirror/state'; |
2 | import { Decoration } from '@codemirror/view'; | 8 | import { Decoration } from '@codemirror/view'; |
3 | 9 | ||