diff options
author | 2024-01-03 18:38:22 +0100 | |
---|---|---|
committer | 2024-01-03 21:14:04 +0100 | |
commit | baa28c9d6b6562a54eee0ad726e22d1b8811751b (patch) | |
tree | 76daca5944872f0b21d6cef472c5cb0b393dff8b /subprojects/frontend/src/editor/GeneratedModelStore.ts | |
parent | refactor(web): subtler error predicate highlight (diff) | |
download | refinery-baa28c9d6b6562a54eee0ad726e22d1b8811751b.tar.gz refinery-baa28c9d6b6562a54eee0ad726e22d1b8811751b.tar.zst refinery-baa28c9d6b6562a54eee0ad726e22d1b8811751b.zip |
feat(web): toggle identifier coloring
Diffstat (limited to 'subprojects/frontend/src/editor/GeneratedModelStore.ts')
-rw-r--r-- | subprojects/frontend/src/editor/GeneratedModelStore.ts | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/subprojects/frontend/src/editor/GeneratedModelStore.ts b/subprojects/frontend/src/editor/GeneratedModelStore.ts index 5088d603..f2695d9a 100644 --- a/subprojects/frontend/src/editor/GeneratedModelStore.ts +++ b/subprojects/frontend/src/editor/GeneratedModelStore.ts | |||
@@ -1,5 +1,5 @@ | |||
1 | /* | 1 | /* |
2 | * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/> | 2 | * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/> |
3 | * | 3 | * |
4 | * SPDX-License-Identifier: EPL-2.0 | 4 | * SPDX-License-Identifier: EPL-2.0 |
5 | */ | 5 | */ |
@@ -9,6 +9,8 @@ import { makeAutoObservable } from 'mobx'; | |||
9 | import GraphStore from '../graph/GraphStore'; | 9 | import GraphStore from '../graph/GraphStore'; |
10 | import type { SemanticsSuccessResult } from '../xtext/xtextServiceResults'; | 10 | import type { SemanticsSuccessResult } from '../xtext/xtextServiceResults'; |
11 | 11 | ||
12 | import type EditorStore from './EditorStore'; | ||
13 | |||
12 | export default class GeneratedModelStore { | 14 | export default class GeneratedModelStore { |
13 | title: string; | 15 | title: string; |
14 | 16 | ||
@@ -18,10 +20,15 @@ export default class GeneratedModelStore { | |||
18 | 20 | ||
19 | graph: GraphStore | undefined; | 21 | graph: GraphStore | undefined; |
20 | 22 | ||
21 | constructor(randomSeed: number) { | 23 | constructor( |
24 | randomSeed: number, | ||
25 | private readonly editorStore: EditorStore, | ||
26 | ) { | ||
22 | const time = new Date().toLocaleTimeString(undefined, { hour12: false }); | 27 | const time = new Date().toLocaleTimeString(undefined, { hour12: false }); |
23 | this.title = `Generated at ${time} (${randomSeed})`; | 28 | this.title = `Generated at ${time} (${randomSeed})`; |
24 | makeAutoObservable(this); | 29 | makeAutoObservable<GeneratedModelStore, 'editorStore'>(this, { |
30 | editorStore: false, | ||
31 | }); | ||
25 | } | 32 | } |
26 | 33 | ||
27 | get running(): boolean { | 34 | get running(): boolean { |
@@ -43,7 +50,7 @@ export default class GeneratedModelStore { | |||
43 | 50 | ||
44 | setSemantics(semantics: SemanticsSuccessResult): void { | 51 | setSemantics(semantics: SemanticsSuccessResult): void { |
45 | if (this.running) { | 52 | if (this.running) { |
46 | this.graph = new GraphStore(); | 53 | this.graph = new GraphStore(this.editorStore); |
47 | this.graph.setSemantics(semantics); | 54 | this.graph.setSemantics(semantics); |
48 | } | 55 | } |
49 | } | 56 | } |