diff options
author | Kristóf Marussy <kristof@marussy.com> | 2022-08-17 21:43:29 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2022-08-17 21:43:29 +0200 |
commit | bb900e1bd40a6b7efd7a538114d985ea7f7e3e88 (patch) | |
tree | bb15a937ade92313dc654a640bc1de925442eff2 /subprojects/frontend/src/editor/createEditorState.ts | |
parent | refactor(frondend): improve editor store and theme (diff) | |
download | refinery-bb900e1bd40a6b7efd7a538114d985ea7f7e3e88.tar.gz refinery-bb900e1bd40a6b7efd7a538114d985ea7f7e3e88.tar.zst refinery-bb900e1bd40a6b7efd7a538114d985ea7f7e3e88.zip |
feat(frontend): custom search panel
Also improves editor styling (to enable panel styling).
Diffstat (limited to 'subprojects/frontend/src/editor/createEditorState.ts')
-rw-r--r-- | subprojects/frontend/src/editor/createEditorState.ts | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/subprojects/frontend/src/editor/createEditorState.ts b/subprojects/frontend/src/editor/createEditorState.ts index 33346c05..caaca7f5 100644 --- a/subprojects/frontend/src/editor/createEditorState.ts +++ b/subprojects/frontend/src/editor/createEditorState.ts | |||
@@ -35,6 +35,7 @@ import { classHighlighter } from '@lezer/highlight'; | |||
35 | import problemLanguageSupport from '../language/problemLanguageSupport'; | 35 | import problemLanguageSupport from '../language/problemLanguageSupport'; |
36 | 36 | ||
37 | import type EditorStore from './EditorStore'; | 37 | import type EditorStore from './EditorStore'; |
38 | import SearchPanel from './SearchPanel'; | ||
38 | import editorClassNames from './editorClassNames'; | 39 | import editorClassNames from './editorClassNames'; |
39 | import findOccurrences from './findOccurrences'; | 40 | import findOccurrences from './findOccurrences'; |
40 | import semanticHighlighting from './semanticHighlighting'; | 41 | import semanticHighlighting from './semanticHighlighting'; |
@@ -61,7 +62,11 @@ export default function createEditorState( | |||
61 | history(), | 62 | history(), |
62 | indentOnInput(), | 63 | indentOnInput(), |
63 | rectangularSelection(), | 64 | rectangularSelection(), |
64 | search({ top: true }), | 65 | search({ |
66 | createPanel(view) { | ||
67 | return new SearchPanel(view, store.searchPanel); | ||
68 | }, | ||
69 | }), | ||
65 | syntaxHighlighting(classHighlighter), | 70 | syntaxHighlighting(classHighlighter), |
66 | semanticHighlighting, | 71 | semanticHighlighting, |
67 | // We add the gutters to `extensions` in the order we want them to appear. | 72 | // We add the gutters to `extensions` in the order we want them to appear. |
@@ -72,8 +77,10 @@ export default function createEditorState( | |||
72 | const button = document.createElement('button'); | 77 | const button = document.createElement('button'); |
73 | button.className = editorClassNames.foldPlaceholder; | 78 | button.className = editorClassNames.foldPlaceholder; |
74 | button.ariaLabel = 'Unfold lines'; | 79 | button.ariaLabel = 'Unfold lines'; |
75 | button.innerText = '...'; | 80 | const span = document.createElement('span'); |
76 | button.onclick = onClick; | 81 | span.innerText = '...'; |
82 | button.appendChild(span); | ||
83 | button.addEventListener('click', onClick); | ||
77 | return button; | 84 | return button; |
78 | }, | 85 | }, |
79 | }), | 86 | }), |