diff options
author | 2021-10-11 01:03:21 +0200 | |
---|---|---|
committer | 2021-10-31 19:26:10 +0100 | |
commit | 299c4d93597b3065e6a1017ebe692cde66fc5e39 (patch) | |
tree | 57d634cec30ca37f0af81a37c3011e027589c35c /language-web/src/main | |
parent | feat(web): add CodeMirror 6 editor (diff) | |
download | refinery-299c4d93597b3065e6a1017ebe692cde66fc5e39.tar.gz refinery-299c4d93597b3065e6a1017ebe692cde66fc5e39.tar.zst refinery-299c4d93597b3065e6a1017ebe692cde66fc5e39.zip |
feat(web): experiment with Lezer parser
Diffstat (limited to 'language-web/src/main')
-rw-r--r-- | language-web/src/main/js/editor/EditorArea.tsx | 49 | ||||
-rw-r--r-- | language-web/src/main/js/editor/EditorParent.ts | 22 | ||||
-rw-r--r-- | language-web/src/main/js/editor/EditorStore.ts | 2 | ||||
-rw-r--r-- | language-web/src/main/js/editor/folding.ts | 97 | ||||
-rw-r--r-- | language-web/src/main/js/editor/indentation.ts | 84 | ||||
-rw-r--r-- | language-web/src/main/js/editor/problem.grammar | 117 | ||||
-rw-r--r-- | language-web/src/main/js/editor/problemLanguageSupport.ts | 82 | ||||
-rw-r--r-- | language-web/src/main/js/index.tsx | 6 |
8 files changed, 441 insertions, 18 deletions
diff --git a/language-web/src/main/js/editor/EditorArea.tsx b/language-web/src/main/js/editor/EditorArea.tsx index 58d65184..460005ce 100644 --- a/language-web/src/main/js/editor/EditorArea.tsx +++ b/language-web/src/main/js/editor/EditorArea.tsx | |||
@@ -1,8 +1,14 @@ | |||
1 | import { Command, EditorView } from '@codemirror/view'; | 1 | import { Command, EditorView } from '@codemirror/view'; |
2 | import { closeSearchPanel, openSearchPanel } from '@codemirror/search'; | 2 | import { closeSearchPanel, openSearchPanel } from '@codemirror/search'; |
3 | import { closeLintPanel, openLintPanel } from '@codemirror/lint'; | 3 | import { closeLintPanel, openLintPanel } from '@codemirror/lint'; |
4 | |||
4 | import { observer } from 'mobx-react-lite'; | 5 | import { observer } from 'mobx-react-lite'; |
5 | import React, { useEffect, useRef, useState } from 'react'; | 6 | import React, { |
7 | useCallback, | ||
8 | useEffect, | ||
9 | useRef, | ||
10 | useState, | ||
11 | } from 'react'; | ||
6 | 12 | ||
7 | import { EditorParent } from './EditorParent'; | 13 | import { EditorParent } from './EditorParent'; |
8 | import { getLogger } from '../logging'; | 14 | import { getLogger } from '../logging'; |
@@ -11,36 +17,49 @@ import { useRootStore } from '../RootStore'; | |||
11 | const log = getLogger('EditorArea'); | 17 | const log = getLogger('EditorArea'); |
12 | 18 | ||
13 | function usePanel( | 19 | function usePanel( |
14 | label: string, | 20 | panelId: string, |
15 | stateToSet: boolean, | 21 | stateToSet: boolean, |
16 | editorView: EditorView | null, | 22 | editorView: EditorView | null, |
17 | openCommand: Command, | 23 | openCommand: Command, |
18 | closeCommand: Command, | 24 | closeCommand: Command, |
25 | closeCallback: () => void, | ||
19 | ) { | 26 | ) { |
20 | const [cachedViewState, setCachedViewState] = useState<boolean>(false); | 27 | const [cachedViewState, setCachedViewState] = useState<boolean>(false); |
21 | useEffect(() => { | 28 | useEffect(() => { |
22 | if (editorView === null || cachedViewState === stateToSet) { | 29 | if (editorView === null || cachedViewState === stateToSet) { |
23 | return; | 30 | return; |
24 | } | 31 | } |
25 | const success = stateToSet ? openCommand(editorView) : closeCommand(editorView); | 32 | if (stateToSet) { |
26 | if (!success) { | 33 | openCommand(editorView); |
27 | log.error( | 34 | const buttonQuery = `.cm-${panelId}.cm-panel button[name="close"]`; |
28 | 'Failed to synchronize', | 35 | const closeButton = editorView.dom.querySelector(buttonQuery); |
29 | label, | 36 | if (closeButton) { |
30 | 'panel state - store state:', | 37 | log.debug('Addig close button callback to', panelId, 'panel'); |
31 | cachedViewState, | 38 | // We must remove the event listener added by CodeMirror from the button |
32 | 'view state:', | 39 | // that dispatches a transaction without going through `EditorStorre`. |
33 | stateToSet, | 40 | // Cloning a DOM node removes event listeners, |
34 | ); | 41 | // see https://stackoverflow.com/a/9251864 |
42 | const closeButtonWithoutListeners = closeButton.cloneNode(true); | ||
43 | closeButtonWithoutListeners.addEventListener('click', (event) => { | ||
44 | closeCallback(); | ||
45 | event.preventDefault(); | ||
46 | }); | ||
47 | closeButton.replaceWith(closeButtonWithoutListeners); | ||
48 | } else { | ||
49 | log.error('Opened', panelId, 'panel has no close button'); | ||
50 | } | ||
51 | } else { | ||
52 | closeCommand(editorView); | ||
35 | } | 53 | } |
36 | setCachedViewState(stateToSet); | 54 | setCachedViewState(stateToSet); |
37 | }, [ | 55 | }, [ |
38 | stateToSet, | 56 | stateToSet, |
39 | editorView, | 57 | editorView, |
40 | cachedViewState, | 58 | cachedViewState, |
41 | label, | 59 | panelId, |
42 | openCommand, | 60 | openCommand, |
43 | closeCommand, | 61 | closeCommand, |
62 | closeCallback, | ||
44 | ]); | 63 | ]); |
45 | return setCachedViewState; | 64 | return setCachedViewState; |
46 | } | 65 | } |
@@ -56,14 +75,16 @@ export const EditorArea = observer(() => { | |||
56 | editorViewState, | 75 | editorViewState, |
57 | openSearchPanel, | 76 | openSearchPanel, |
58 | closeSearchPanel, | 77 | closeSearchPanel, |
78 | useCallback(() => editorStore.setSearchPanelOpen(false), [editorStore]), | ||
59 | ); | 79 | ); |
60 | 80 | ||
61 | const setLintPanelOpen = usePanel( | 81 | const setLintPanelOpen = usePanel( |
62 | 'lint', | 82 | 'panel-lint', |
63 | editorStore.showLintPanel, | 83 | editorStore.showLintPanel, |
64 | editorViewState, | 84 | editorViewState, |
65 | openLintPanel, | 85 | openLintPanel, |
66 | closeLintPanel, | 86 | closeLintPanel, |
87 | useCallback(() => editorStore.setLintPanelOpen(false), [editorStore]), | ||
67 | ); | 88 | ); |
68 | 89 | ||
69 | useEffect(() => { | 90 | useEffect(() => { |
diff --git a/language-web/src/main/js/editor/EditorParent.ts b/language-web/src/main/js/editor/EditorParent.ts index bf67522b..316c5072 100644 --- a/language-web/src/main/js/editor/EditorParent.ts +++ b/language-web/src/main/js/editor/EditorParent.ts | |||
@@ -49,13 +49,29 @@ export const EditorParent = styled('div')(({ theme }) => ({ | |||
49 | background: theme.palette.background.paper, | 49 | background: theme.palette.background.paper, |
50 | borderTop: `1px solid ${theme.palette.divider}`, | 50 | borderTop: `1px solid ${theme.palette.divider}`, |
51 | 'button[name="close"]': { | 51 | 'button[name="close"]': { |
52 | // HACK We can't hook the panel close button to go through `EditorStore`, | 52 | color: theme.palette.text.secondary, |
53 | // so we hide it altogether. | 53 | cursor: 'pointer', |
54 | display: 'none', | ||
55 | }, | 54 | }, |
56 | }, | 55 | }, |
56 | '.cm-foldPlaceholder': { | ||
57 | background: theme.palette.background.paper, | ||
58 | borderColor: theme.palette.text.disabled, | ||
59 | color: theme.palette.text.secondary, | ||
60 | }, | ||
57 | '.cmt-comment': { | 61 | '.cmt-comment': { |
58 | fontVariant: 'italic', | 62 | fontVariant: 'italic', |
59 | color: theme.palette.text.disabled, | 63 | color: theme.palette.text.disabled, |
60 | }, | 64 | }, |
65 | '.cmt-number': { | ||
66 | color: '#6188a6', | ||
67 | }, | ||
68 | '.cmt-keyword': { | ||
69 | color: theme.palette.primary.main, | ||
70 | }, | ||
71 | '.cmt-typeName, .cmt-atom': { | ||
72 | color: theme.palette.text.primary, | ||
73 | }, | ||
74 | '.cmt-variableName': { | ||
75 | color: '#c8ae9d', | ||
76 | }, | ||
61 | })); | 77 | })); |
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts index 326c02a1..eb358338 100644 --- a/language-web/src/main/js/editor/EditorStore.ts +++ b/language-web/src/main/js/editor/EditorStore.ts | |||
@@ -39,6 +39,7 @@ import { | |||
39 | } from 'mobx'; | 39 | } from 'mobx'; |
40 | 40 | ||
41 | import { getLogger } from '../logging'; | 41 | import { getLogger } from '../logging'; |
42 | import { problemLanguageSupport } from './problemLanguageSupport'; | ||
42 | import type { ThemeStore } from '../theme/ThemeStore'; | 43 | import type { ThemeStore } from '../theme/ThemeStore'; |
43 | 44 | ||
44 | const log = getLogger('EditorStore'); | 45 | const log = getLogger('EditorStore'); |
@@ -105,6 +106,7 @@ export class EditorStore { | |||
105 | ...searchKeymap, | 106 | ...searchKeymap, |
106 | ...defaultKeymap, | 107 | ...defaultKeymap, |
107 | ]), | 108 | ]), |
109 | problemLanguageSupport(), | ||
108 | ], | 110 | ], |
109 | }); | 111 | }); |
110 | reaction( | 112 | reaction( |
diff --git a/language-web/src/main/js/editor/folding.ts b/language-web/src/main/js/editor/folding.ts new file mode 100644 index 00000000..54c7294d --- /dev/null +++ b/language-web/src/main/js/editor/folding.ts | |||
@@ -0,0 +1,97 @@ | |||
1 | import { EditorState } from '@codemirror/state'; | ||
2 | import type { SyntaxNode } from '@lezer/common'; | ||
3 | |||
4 | export type FoldRange = { from: number, to: number }; | ||
5 | |||
6 | /** | ||
7 | * Folds a block comment between its delimiters. | ||
8 | * | ||
9 | * @param node the node to fold | ||
10 | * @returns the folding range or `null` is there is nothing to fold | ||
11 | */ | ||
12 | export function foldBlockComment(node: SyntaxNode): FoldRange { | ||
13 | return { | ||
14 | from: node.from + 2, | ||
15 | to: node.to - 2, | ||
16 | }; | ||
17 | } | ||
18 | |||
19 | /** | ||
20 | * Folds a declaration after the first element if it appears on the opening line, | ||
21 | * otherwise folds after the opening keyword. | ||
22 | * | ||
23 | * @example | ||
24 | * First element on the opening line: | ||
25 | * ``` | ||
26 | * scope Family = 1, | ||
27 | * Person += 5..10. | ||
28 | * ``` | ||
29 | * becomes | ||
30 | * ``` | ||
31 | * scope Family = 1,[...]. | ||
32 | * ``` | ||
33 | * | ||
34 | * @example | ||
35 | * First element not on the opening line: | ||
36 | * ``` | ||
37 | * scope Family | ||
38 | * = 1, | ||
39 | * Person += 5..10. | ||
40 | * ``` | ||
41 | * becomes | ||
42 | * ``` | ||
43 | * scope [...]. | ||
44 | * ``` | ||
45 | * | ||
46 | * @param node the node to fold | ||
47 | * @param state the editor state | ||
48 | * @returns the folding range or `null` is there is nothing to fold | ||
49 | */ | ||
50 | export function foldDeclaration(node: SyntaxNode, state: EditorState): FoldRange | null { | ||
51 | const { firstChild: open, lastChild: close } = node; | ||
52 | if (open === null || close === null) { | ||
53 | return null; | ||
54 | } | ||
55 | const { cursor } = open; | ||
56 | const lineEnd = state.doc.lineAt(open.from).to; | ||
57 | let foldFrom = open.to; | ||
58 | while (cursor.next() && cursor.from < lineEnd) { | ||
59 | if (cursor.type.name === ',') { | ||
60 | foldFrom = cursor.to; | ||
61 | break; | ||
62 | } | ||
63 | } | ||
64 | return { | ||
65 | from: foldFrom, | ||
66 | to: close.from, | ||
67 | }; | ||
68 | } | ||
69 | |||
70 | /** | ||
71 | * Folds a node only if it has at least one sibling of the same type. | ||
72 | * | ||
73 | * The folding range will be the entire `node`. | ||
74 | * | ||
75 | * @param node the node to fold | ||
76 | * @returns the folding range or `null` is there is nothing to fold | ||
77 | */ | ||
78 | export function foldConjunction(node: SyntaxNode): FoldRange | null { | ||
79 | const { parent } = node; | ||
80 | if (parent === null) { | ||
81 | return null; | ||
82 | } | ||
83 | const { cursor } = parent; | ||
84 | let nConjunctions = 0; | ||
85 | while (cursor.next()) { | ||
86 | if (cursor.type === node.type) { | ||
87 | nConjunctions += 1; | ||
88 | } | ||
89 | if (nConjunctions >= 2) { | ||
90 | return { | ||
91 | from: node.from, | ||
92 | to: node.to, | ||
93 | }; | ||
94 | } | ||
95 | } | ||
96 | return null; | ||
97 | } | ||
diff --git a/language-web/src/main/js/editor/indentation.ts b/language-web/src/main/js/editor/indentation.ts new file mode 100644 index 00000000..b2f0134b --- /dev/null +++ b/language-web/src/main/js/editor/indentation.ts | |||
@@ -0,0 +1,84 @@ | |||
1 | import { TreeIndentContext } from '@codemirror/language'; | ||
2 | |||
3 | /** | ||
4 | * Finds the `from` of first non-skipped token, if any, | ||
5 | * after the opening keyword in the first line of the declaration. | ||
6 | * | ||
7 | * Based on | ||
8 | * https://github.com/codemirror/language/blob/cd7f7e66fa51ddbce96cf9396b1b6127d0ca4c94/src/indent.ts#L246 | ||
9 | * | ||
10 | * @param context the indentation context | ||
11 | * @returns the alignment or `null` if there is no token after the opening keyword | ||
12 | */ | ||
13 | function findAlignmentAfterOpening(context: TreeIndentContext): number | null { | ||
14 | const { | ||
15 | node: tree, | ||
16 | simulatedBreak, | ||
17 | } = context; | ||
18 | const openingToken = tree.childAfter(tree.from); | ||
19 | if (openingToken === null) { | ||
20 | return null; | ||
21 | } | ||
22 | const openingLine = context.state.doc.lineAt(openingToken.from); | ||
23 | const lineEnd = simulatedBreak == null || simulatedBreak <= openingLine.from | ||
24 | ? openingLine.to | ||
25 | : Math.min(openingLine.to, simulatedBreak); | ||
26 | const { cursor } = openingToken; | ||
27 | while (cursor.next() && cursor.from < lineEnd) { | ||
28 | if (!cursor.type.isSkipped) { | ||
29 | return cursor.from; | ||
30 | } | ||
31 | } | ||
32 | return null; | ||
33 | } | ||
34 | |||
35 | /** | ||
36 | * Indents text after declarations by a single unit if it begins on a new line, | ||
37 | * otherwise it aligns with the text after the declaration. | ||
38 | * | ||
39 | * Based on | ||
40 | * https://github.com/codemirror/language/blob/cd7f7e66fa51ddbce96cf9396b1b6127d0ca4c94/src/indent.ts#L275 | ||
41 | * | ||
42 | * @example | ||
43 | * Result with no hanging indent (indent unit = 2 spaces, units = 1): | ||
44 | * ``` | ||
45 | * scope | ||
46 | * Family = 1, | ||
47 | * Person += 5..10. | ||
48 | * ``` | ||
49 | * | ||
50 | * @example | ||
51 | * Result with hanging indent: | ||
52 | * ``` | ||
53 | * scope Family = 1, | ||
54 | * Person += 5..10. | ||
55 | * ``` | ||
56 | * | ||
57 | * @param context the indentation context | ||
58 | * @param units the number of units to indent | ||
59 | * @returns the desired indentation level | ||
60 | */ | ||
61 | function indentDeclarationStrategy(context: TreeIndentContext, units: number): number { | ||
62 | const alignment = findAlignmentAfterOpening(context); | ||
63 | if (alignment !== null) { | ||
64 | return context.column(alignment); | ||
65 | } | ||
66 | return context.baseIndent + units * context.unit; | ||
67 | } | ||
68 | |||
69 | export function indentBlockComment(): number { | ||
70 | // Do not indent. | ||
71 | return -1; | ||
72 | } | ||
73 | |||
74 | export function indentDeclaration(context: TreeIndentContext): number { | ||
75 | return indentDeclarationStrategy(context, 1); | ||
76 | } | ||
77 | |||
78 | export function indentPredicate(context: TreeIndentContext): number { | ||
79 | const clauseIndent = indentDeclarationStrategy(context, 1); | ||
80 | if (/^\s+(;|\.)/.exec(context.textAfter) !== null) { | ||
81 | return clauseIndent - context.unit; | ||
82 | } | ||
83 | return clauseIndent; | ||
84 | } | ||
diff --git a/language-web/src/main/js/editor/problem.grammar b/language-web/src/main/js/editor/problem.grammar new file mode 100644 index 00000000..c64402b0 --- /dev/null +++ b/language-web/src/main/js/editor/problem.grammar | |||
@@ -0,0 +1,117 @@ | |||
1 | |||
2 | @top Problem { statement* } | ||
3 | |||
4 | statement { | ||
5 | ProblemDeclaration { | ||
6 | kw<"problem"> QualifiedName "." | ||
7 | } | | ||
8 | ClassDefinition { | ||
9 | kw<"abstract">? kw<"class"> RelationName | ||
10 | (ClassBody { "{" ReferenceDeclaration* "}" } | ".") | ||
11 | } | | ||
12 | EnumDefinition { | ||
13 | kw<"enum"> RelationName | ||
14 | (EnumBody { "{" sep<",", UniqueNodeName> "}" } | ".") | ||
15 | } | | ||
16 | PredicateDefinition { | ||
17 | (kw<"error"> kw<"pred">? | kw<"pred">) RelationName ParameterList<Parameter>? | ||
18 | PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." } | ||
19 | } | | ||
20 | Assertion { | ||
21 | kw<"default">? (NotOp | UnknownOp)? RelationName | ||
22 | ParameterList<AssertionArgument> (":" LogicValue)? "." | ||
23 | } | | ||
24 | UniqueDeclaration { | ||
25 | kw<"unique"> sep<",", UniqueNodeName> "." | ||
26 | } | | ||
27 | ScopeDeclaration { | ||
28 | kw<"scope"> sep<",", ScopeElement> "." | ||
29 | } | ||
30 | } | ||
31 | |||
32 | ReferenceDeclaration { | ||
33 | (kw<"refers"> | kw<"contains">)? | ||
34 | RelationName | ||
35 | RelationName | ||
36 | ( "[" Multiplicity? "]" )? | ||
37 | (kw<"opposite"> RelationName)? | ||
38 | ";"? | ||
39 | } | ||
40 | |||
41 | Parameter { RelationName? VariableName } | ||
42 | |||
43 | Conjunction { sep1<",", Literal> } | ||
44 | |||
45 | OrOp { ";" } | ||
46 | |||
47 | Literal { NotOp? Atom } | ||
48 | |||
49 | Atom { RelationName ParameterList<Argument>? } | ||
50 | |||
51 | Argument { VariableName | Real } | ||
52 | |||
53 | AssertionArgument { NodeName | StarArgument | Real } | ||
54 | |||
55 | LogicValue { | ||
56 | kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error"> | ||
57 | } | ||
58 | |||
59 | ScopeElement { RelationName ("=" | "+=") Multiplicity } | ||
60 | |||
61 | Multiplicity { (IntMult "..")? (IntMult | StarMult)} | ||
62 | |||
63 | RelationName { QualifiedName } | ||
64 | |||
65 | UniqueNodeName { QualifiedName } | ||
66 | |||
67 | VariableName { QualifiedName } | ||
68 | |||
69 | NodeName { QualifiedName } | ||
70 | |||
71 | QualifiedName { identifier ("::" identifier)* } | ||
72 | |||
73 | kw<term> { @specialize[@name={term}]<identifier, term> } | ||
74 | |||
75 | ParameterList<content> { "(" sep<",", content> ")" } | ||
76 | |||
77 | sep<separator, content> { sep1<separator, content>? } | ||
78 | |||
79 | sep1<separator, content> { content (separator content?)* } | ||
80 | |||
81 | @skip { LineComment | BlockComment | whitespace } | ||
82 | |||
83 | @tokens { | ||
84 | whitespace { std.whitespace+ } | ||
85 | |||
86 | LineComment { ("//" | "%") ![\n]* } | ||
87 | |||
88 | BlockComment { "/*" blockCommentRest } | ||
89 | |||
90 | blockCommentRest { ![*] blockCommentRest | "*" blockCommentAfterStar } | ||
91 | |||
92 | blockCommentAfterStar { "/" | "*" blockCommentAfterStar | ![/*] blockCommentRest } | ||
93 | |||
94 | @precedence { BlockComment, LineComment } | ||
95 | |||
96 | identifier { $[A-Za-z_] $[a-zA-Z0-9_]* } | ||
97 | |||
98 | int { $[0-9]+ } | ||
99 | |||
100 | IntMult { int } | ||
101 | |||
102 | StarMult { "*" } | ||
103 | |||
104 | Real { "-"? (exponential | int ("." (int | exponential))?) } | ||
105 | |||
106 | exponential { int ("e" | "E") ("+" | "-")? int } | ||
107 | |||
108 | NotOp { "!" } | ||
109 | |||
110 | UnknownOp { "?" } | ||
111 | |||
112 | StarArgument { "*" } | ||
113 | |||
114 | "{" "}" "(" ")" "[" "]" "." ".." "," ":" "<->" | ||
115 | } | ||
116 | |||
117 | @detectDelim | ||
diff --git a/language-web/src/main/js/editor/problemLanguageSupport.ts b/language-web/src/main/js/editor/problemLanguageSupport.ts new file mode 100644 index 00000000..2bf7c7a4 --- /dev/null +++ b/language-web/src/main/js/editor/problemLanguageSupport.ts | |||
@@ -0,0 +1,82 @@ | |||
1 | import { styleTags, tags as t } from '@codemirror/highlight'; | ||
2 | import { | ||
3 | foldInside, | ||
4 | foldNodeProp, | ||
5 | indentNodeProp, | ||
6 | LanguageSupport, | ||
7 | LRLanguage, | ||
8 | } from '@codemirror/language'; | ||
9 | import { LRParser } from '@lezer/lr'; | ||
10 | |||
11 | import { parser } from '../../../../build/generated/sources/lezer/problem'; | ||
12 | import { | ||
13 | foldBlockComment, | ||
14 | foldConjunction, | ||
15 | foldDeclaration, | ||
16 | } from './folding'; | ||
17 | import { | ||
18 | indentBlockComment, | ||
19 | indentDeclaration, | ||
20 | indentPredicate, | ||
21 | } from './indentation'; | ||
22 | |||
23 | const parserWithMetadata = (parser as LRParser).configure({ | ||
24 | props: [ | ||
25 | styleTags({ | ||
26 | LineComment: t.lineComment, | ||
27 | BlockComment: t.blockComment, | ||
28 | 'problem class enum pred unique scope': t.definitionKeyword, | ||
29 | 'abstract refers contains opposite error default': t.modifier, | ||
30 | 'true false unknown error': t.keyword, | ||
31 | NotOp: t.keyword, | ||
32 | UnknownOp: t.keyword, | ||
33 | OrOp: t.keyword, | ||
34 | StarArgument: t.keyword, | ||
35 | 'IntMult StarMult Real': t.number, | ||
36 | StarMult: t.number, | ||
37 | 'RelationName/QualifiedName': t.typeName, | ||
38 | 'UniqueNodeName/QualifiedName': t.atom, | ||
39 | 'VariableName/QualifiedName': t.variableName, | ||
40 | '{ }': t.brace, | ||
41 | '( )': t.paren, | ||
42 | '[ ]': t.squareBracket, | ||
43 | '. .. , :': t.separator, | ||
44 | '<->': t.definitionOperator, | ||
45 | }), | ||
46 | indentNodeProp.add({ | ||
47 | ProblemDeclaration: indentDeclaration, | ||
48 | UniqueDeclaration: indentDeclaration, | ||
49 | ScopeDeclaration: indentDeclaration, | ||
50 | PredicateBody: indentPredicate, | ||
51 | BlockComment: indentBlockComment, | ||
52 | }), | ||
53 | foldNodeProp.add({ | ||
54 | ClassBody: foldInside, | ||
55 | EnumBody: foldInside, | ||
56 | ParameterList: foldInside, | ||
57 | PredicateBody: foldInside, | ||
58 | Conjunction: foldConjunction, | ||
59 | UniqueDeclaration: foldDeclaration, | ||
60 | ScopeDeclaration: foldDeclaration, | ||
61 | BlockComment: foldBlockComment, | ||
62 | }), | ||
63 | ], | ||
64 | }); | ||
65 | |||
66 | const problemLanguage = LRLanguage.define({ | ||
67 | parser: parserWithMetadata, | ||
68 | languageData: { | ||
69 | commentTokens: { | ||
70 | block: { | ||
71 | open: '/*', | ||
72 | close: '*/', | ||
73 | }, | ||
74 | line: '%', | ||
75 | }, | ||
76 | indentOnInput: /^\s*(?:\{|\}|\(|\)|;|\.)$/, | ||
77 | }, | ||
78 | }); | ||
79 | |||
80 | export function problemLanguageSupport(): LanguageSupport { | ||
81 | return new LanguageSupport(problemLanguage); | ||
82 | } | ||
diff --git a/language-web/src/main/js/index.tsx b/language-web/src/main/js/index.tsx index 66ad1f28..1b24eadb 100644 --- a/language-web/src/main/js/index.tsx +++ b/language-web/src/main/js/index.tsx | |||
@@ -25,7 +25,11 @@ enum TaxStatus { | |||
25 | 25 | ||
26 | % A child cannot have any dependents. | 26 | % A child cannot have any dependents. |
27 | error invalidTaxStatus(Person p) <-> | 27 | error invalidTaxStatus(Person p) <-> |
28 | taxStatus(p, child), children(p, _q). | 28 | taxStatus(p, child), |
29 | children(p, _q) | ||
30 | ; taxStatus(p, retired), | ||
31 | parent(p, q), | ||
32 | !taxStatus(q, retired). | ||
29 | 33 | ||
30 | unique family. | 34 | unique family. |
31 | Family(family). | 35 | Family(family). |