diff options
author | 2021-10-30 20:14:50 +0200 | |
---|---|---|
committer | 2021-10-31 19:26:14 +0100 | |
commit | cbf442d8fd9f72c567ebf9f036a219a9ff100487 (patch) | |
tree | a128345d9a9863bef7f3670da585bcb62d13cb34 /language-web/src/main/js/editor/EditorStore.ts | |
parent | feat(web): show error count on generate button (diff) | |
download | refinery-cbf442d8fd9f72c567ebf9f036a219a9ff100487.tar.gz refinery-cbf442d8fd9f72c567ebf9f036a219a9ff100487.tar.zst refinery-cbf442d8fd9f72c567ebf9f036a219a9ff100487.zip |
feat(web): semantic highlighting
Diffstat (limited to 'language-web/src/main/js/editor/EditorStore.ts')
-rw-r--r-- | language-web/src/main/js/editor/EditorStore.ts | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts index 78cf763c..f47f47a0 100644 --- a/language-web/src/main/js/editor/EditorStore.ts +++ b/language-web/src/main/js/editor/EditorStore.ts | |||
@@ -30,6 +30,7 @@ import { | |||
30 | TransactionSpec, | 30 | TransactionSpec, |
31 | } from '@codemirror/state'; | 31 | } from '@codemirror/state'; |
32 | import { | 32 | import { |
33 | DecorationSet, | ||
33 | drawSelection, | 34 | drawSelection, |
34 | EditorView, | 35 | EditorView, |
35 | highlightActiveLine, | 36 | highlightActiveLine, |
@@ -43,8 +44,9 @@ import { | |||
43 | } from 'mobx'; | 44 | } from 'mobx'; |
44 | 45 | ||
45 | import { problemLanguageSupport } from '../language/problemLanguageSupport'; | 46 | import { problemLanguageSupport } from '../language/problemLanguageSupport'; |
46 | import { getLogger } from '../utils/logger'; | 47 | import { semanticHighlighting, setSemanticHighlighting } from './semanticHighlighting'; |
47 | import type { ThemeStore } from '../theme/ThemeStore'; | 48 | import type { ThemeStore } from '../theme/ThemeStore'; |
49 | import { getLogger } from '../utils/logger'; | ||
48 | import { XtextClient } from '../xtext/XtextClient'; | 50 | import { XtextClient } from '../xtext/XtextClient'; |
49 | 51 | ||
50 | const log = getLogger('editor.EditorStore'); | 52 | const log = getLogger('editor.EditorStore'); |
@@ -103,6 +105,7 @@ export class EditorStore { | |||
103 | top: true, | 105 | top: true, |
104 | matchCase: true, | 106 | matchCase: true, |
105 | }), | 107 | }), |
108 | semanticHighlighting, | ||
106 | // We add the gutters to `extensions` in the order we want them to appear. | 109 | // We add the gutters to `extensions` in the order we want them to appear. |
107 | foldGutter(), | 110 | foldGutter(), |
108 | lineNumbers(), | 111 | lineNumbers(), |
@@ -201,6 +204,10 @@ export class EditorStore { | |||
201 | return null; | 204 | return null; |
202 | } | 205 | } |
203 | 206 | ||
207 | updateSemanticHighlighting(decorations: DecorationSet): void { | ||
208 | this.dispatch(setSemanticHighlighting(decorations)); | ||
209 | } | ||
210 | |||
204 | /** | 211 | /** |
205 | * @returns `true` if there is history to undo | 212 | * @returns `true` if there is history to undo |
206 | */ | 213 | */ |