diff options
-rw-r--r-- | .editorconfig | 2 | ||||
-rw-r--r-- | language-web/build.gradle | 12 | ||||
-rw-r--r-- | language-web/package.json | 5 | ||||
-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 | ||||
-rw-r--r-- | language-web/tsconfig.json | 4 | ||||
-rw-r--r-- | language-web/yarn.lock | 10 |
13 files changed, 468 insertions, 24 deletions
diff --git a/.editorconfig b/.editorconfig index 5ce3abdf..60e56bf7 100644 --- a/.editorconfig +++ b/.editorconfig | |||
@@ -10,6 +10,6 @@ insert_final_newline = true | |||
10 | indent_style = tab | 10 | indent_style = tab |
11 | indent_size = 4 | 11 | indent_size = 4 |
12 | 12 | ||
13 | [*.{html,js,json,jsx,scss,ts,tsx,yml}] | 13 | [*.{grammar,html,js,json,jsx,scss,ts,tsx,yml}] |
14 | indent_style = space | 14 | indent_style = space |
15 | indent_size = 2 | 15 | indent_size = 2 |
diff --git a/language-web/build.gradle b/language-web/build.gradle index c467c019..1f1457d6 100644 --- a/language-web/build.gradle +++ b/language-web/build.gradle | |||
@@ -35,14 +35,24 @@ frontend { | |||
35 | yarnEnabled = true | 35 | yarnEnabled = true |
36 | yarnVersion = project.ext.yarnVersion | 36 | yarnVersion = project.ext.yarnVersion |
37 | yarnInstallDirectory = file("${rootDir}/.gradle/yarn") | 37 | yarnInstallDirectory = file("${rootDir}/.gradle/yarn") |
38 | assembleScript = 'run assemble' | 38 | assembleScript = 'run assemble:webpack' |
39 | } | 39 | } |
40 | 40 | ||
41 | def installFrontend = tasks.named('installFrontend') | 41 | def installFrontend = tasks.named('installFrontend') |
42 | 42 | ||
43 | def generateLezerGrammar = tasks.register('generateLezerGrammar', RunNpmYarn) { | ||
44 | dependsOn installFrontend | ||
45 | inputs.file('src/main/js/editor/problem.grammar') | ||
46 | inputs.files('package.json', 'yarn.lock') | ||
47 | outputs.file "${buildDir}/generated/sources/lezer/problem.ts" | ||
48 | outputs.file "${buildDir}/generated/sources/lezer/problem.terms.ts" | ||
49 | script = 'run assemble:lezer' | ||
50 | } | ||
51 | |||
43 | def assembleFrontend = tasks.named('assembleFrontend') | 52 | def assembleFrontend = tasks.named('assembleFrontend') |
44 | assembleFrontend.configure { | 53 | assembleFrontend.configure { |
45 | dependsOn generateXtextLanguage | 54 | dependsOn generateXtextLanguage |
55 | dependsOn generateLezerGrammar | ||
46 | inputs.dir 'src/main/css' | 56 | inputs.dir 'src/main/css' |
47 | inputs.dir 'src/main/html' | 57 | inputs.dir 'src/main/html' |
48 | inputs.dir 'src/main/js' | 58 | inputs.dir 'src/main/js' |
diff --git a/language-web/package.json b/language-web/package.json index d55968ee..78b080ee 100644 --- a/language-web/package.json +++ b/language-web/package.json | |||
@@ -4,7 +4,8 @@ | |||
4 | "description": "Web frontend for VIATRA-Generator", | 4 | "description": "Web frontend for VIATRA-Generator", |
5 | "main": "index.js", | 5 | "main": "index.js", |
6 | "scripts": { | 6 | "scripts": { |
7 | "assemble": "webpack --node-env production", | 7 | "assemble:lezer": "lezer-generator src/main/js/editor/problem.grammar -o build/generated/sources/lezer/problem.ts", |
8 | "assemble:webpack": "webpack --node-env production", | ||
8 | "serve": "webpack serve --node-env development --hot", | 9 | "serve": "webpack serve --node-env development --hot", |
9 | "check": "yarn run check:eslint && yarn run check:stylelint", | 10 | "check": "yarn run check:eslint && yarn run check:stylelint", |
10 | "check:eslint": "eslint .", | 11 | "check:eslint": "eslint .", |
@@ -40,6 +41,7 @@ | |||
40 | "eslint-plugin-sonarjs": "^0.10.0", | 41 | "eslint-plugin-sonarjs": "^0.10.0", |
41 | "html-webpack-plugin": "^5.3.2", | 42 | "html-webpack-plugin": "^5.3.2", |
42 | "image-webpack-loader": "^8.0.1", | 43 | "image-webpack-loader": "^8.0.1", |
44 | "@lezer/generator": "^0.15.2", | ||
43 | "magic-comments-loader": "^1.4.1", | 45 | "magic-comments-loader": "^1.4.1", |
44 | "mini-css-extract-plugin": "^2.3.0", | 46 | "mini-css-extract-plugin": "^2.3.0", |
45 | "@principalstudio/html-webpack-inject-preload": "^1.2.7", | 47 | "@principalstudio/html-webpack-inject-preload": "^1.2.7", |
@@ -81,6 +83,7 @@ | |||
81 | "@emotion/styled": "^11.3.0", | 83 | "@emotion/styled": "^11.3.0", |
82 | "@fontsource/jetbrains-mono": "^4.5.0", | 84 | "@fontsource/jetbrains-mono": "^4.5.0", |
83 | "@fontsource/roboto": "^4.5.0", | 85 | "@fontsource/roboto": "^4.5.0", |
86 | "@lezer/lr": "^0.15.4", | ||
84 | "@mui/material": "5.0.2", | 87 | "@mui/material": "5.0.2", |
85 | "@mui/icons-material": "5.0.1", | 88 | "@mui/icons-material": "5.0.1", |
86 | "jquery": "^3.6.0", | 89 | "jquery": "^3.6.0", |
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). |
diff --git a/language-web/tsconfig.json b/language-web/tsconfig.json index 7f43a8b5..d028a64f 100644 --- a/language-web/tsconfig.json +++ b/language-web/tsconfig.json | |||
@@ -4,7 +4,7 @@ | |||
4 | "module": "ES2020", | 4 | "module": "ES2020", |
5 | "moduleResolution": "node", | 5 | "moduleResolution": "node", |
6 | "paths": { | 6 | "paths": { |
7 | "xtext/*": ["./src/main/js/xtext/*"] | 7 | "xtext/*": ["./src/main/js/xtext/*"], |
8 | }, | 8 | }, |
9 | "esModuleInterop": true, | 9 | "esModuleInterop": true, |
10 | "allowSyntheticDefaultImports": true, | 10 | "allowSyntheticDefaultImports": true, |
@@ -16,5 +16,5 @@ | |||
16 | "noEmit": true | 16 | "noEmit": true |
17 | }, | 17 | }, |
18 | "include": ["./src/main/js/**/*"], | 18 | "include": ["./src/main/js/**/*"], |
19 | "exclude": ["./src/main/js/xtext/**/*"] | 19 | "exclude": ["./build/generated/sources/lezer/*"] |
20 | } | 20 | } |
diff --git a/language-web/yarn.lock b/language-web/yarn.lock index 51c551a7..360c5be3 100644 --- a/language-web/yarn.lock +++ b/language-web/yarn.lock | |||
@@ -1305,7 +1305,15 @@ | |||
1305 | resolved "https://registry.yarnpkg.com/@lezer/common/-/common-0.15.7.tgz#8b445dae9777f689783132cf490770ece3c03d7b" | 1305 | resolved "https://registry.yarnpkg.com/@lezer/common/-/common-0.15.7.tgz#8b445dae9777f689783132cf490770ece3c03d7b" |
1306 | integrity sha512-Rw8TDJnBzZnkyzIXs1Tmmd241FrBLJBj8gkdy3y0joGFb8Z4I/joKEsR+gv1pb13o1TMsZxm3fmP+d/wPt2CTQ== | 1306 | integrity sha512-Rw8TDJnBzZnkyzIXs1Tmmd241FrBLJBj8gkdy3y0joGFb8Z4I/joKEsR+gv1pb13o1TMsZxm3fmP+d/wPt2CTQ== |
1307 | 1307 | ||
1308 | "@lezer/lr@^0.15.0": | 1308 | "@lezer/generator@^0.15.2": |
1309 | version "0.15.2" | ||
1310 | resolved "https://registry.yarnpkg.com/@lezer/generator/-/generator-0.15.2.tgz#10fa8fab58a561c2bd2a27d7b4f20b1080c6cb6c" | ||
1311 | integrity sha512-nxY6TTj0ZAcAvg1zEeaZnt1xODdyPhD0lTaPOgcGOVFHhwwx0Oz7CxZB7Rh+xRCXFr5kJWDtM1uXPp80UZjhAg== | ||
1312 | dependencies: | ||
1313 | "@lezer/common" "^0.15.0" | ||
1314 | "@lezer/lr" "^0.15.0" | ||
1315 | |||
1316 | "@lezer/lr@^0.15.0", "@lezer/lr@^0.15.4": | ||
1309 | version "0.15.4" | 1317 | version "0.15.4" |
1310 | resolved "https://registry.yarnpkg.com/@lezer/lr/-/lr-0.15.4.tgz#634670d7224040fddac1370af01211eecd9ac0a0" | 1318 | resolved "https://registry.yarnpkg.com/@lezer/lr/-/lr-0.15.4.tgz#634670d7224040fddac1370af01211eecd9ac0a0" |
1311 | integrity sha512-vwgG80sihEGJn6wJp6VijXrnzVai/KPva/OzYKaWvIx0IiXKjoMQ8UAwcgpSBwfS4Fbz3IKOX/cCNXU3r1FvpQ== | 1319 | integrity sha512-vwgG80sihEGJn6wJp6VijXrnzVai/KPva/OzYKaWvIx0IiXKjoMQ8UAwcgpSBwfS4Fbz3IKOX/cCNXU3r1FvpQ== |