diff options
Diffstat (limited to 'language-web/src')
9 files changed, 213 insertions, 39 deletions
diff --git a/language-web/src/main/css/index.scss b/language-web/src/main/css/index.scss index 9d6e0f6a..54f3a654 100644 --- a/language-web/src/main/css/index.scss +++ b/language-web/src/main/css/index.scss | |||
@@ -30,12 +30,27 @@ body { | |||
30 | height: 100%; | 30 | height: 100%; |
31 | } | 31 | } |
32 | 32 | ||
33 | .CodeMirror, .CodeMirror-hints { | 33 | .problem-fallback-editor { |
34 | display: block; | ||
35 | height: 100%; | ||
36 | width: 100%; | ||
37 | resize: none; | ||
38 | border: none; | ||
39 | outline: none; | ||
40 | padding: 4px 4px 4px 16px; | ||
41 | white-space: pre; | ||
42 | overflow-wrap: normal; | ||
43 | overflow: auto; | ||
44 | } | ||
45 | |||
46 | .CodeMirror, .CodeMirror-hints, .problem-fallback-editor { | ||
34 | font-size: 16px; | 47 | font-size: 16px; |
35 | font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace; | 48 | font-family: 'JetBrains MonoVariable', 'JetBrains Mono', monospace; |
36 | font-feature-settings: 'liga', 'calt'; | 49 | font-feature-settings: 'liga', 'calt'; |
37 | font-weight: 400; | 50 | font-weight: 400; |
38 | text-rendering: optimizeLegibility; | 51 | text-rendering: optimizeLegibility; |
52 | line-height: 1.35; | ||
53 | letter-spacing: 0; | ||
39 | } | 54 | } |
40 | 55 | ||
41 | @each $themeName, $theme in $themes { | 56 | @each $themeName, $theme in $themes { |
@@ -45,6 +60,16 @@ body { | |||
45 | color: map.get($theme, 'foreground'); | 60 | color: map.get($theme, 'foreground'); |
46 | } | 61 | } |
47 | 62 | ||
63 | &.problem-fallback-editor { | ||
64 | background: map.get($theme, 'background'); | ||
65 | color: map.get($theme, 'foreground'); | ||
66 | caret-color: map.get($theme, 'cursor'); | ||
67 | |||
68 | &::selection { | ||
69 | background: map.get($theme, 'selection'); | ||
70 | } | ||
71 | } | ||
72 | |||
48 | .CodeMirror-gutters { | 73 | .CodeMirror-gutters { |
49 | background: map.get($theme, 'background'); | 74 | background: map.get($theme, 'background'); |
50 | border: none; | 75 | border: none; |
@@ -183,11 +208,13 @@ li.CodeMirror-hint-active { | |||
183 | 208 | ||
184 | .xtext-marker_read { | 209 | .xtext-marker_read { |
185 | background: rgba(128, 203, 196, 0.2); | 210 | background: rgba(128, 203, 196, 0.2); |
211 | display: inline-block; | ||
186 | } | 212 | } |
187 | 213 | ||
188 | 214 | ||
189 | .xtext-marker_write { | 215 | .xtext-marker_write { |
190 | background: rgba(255, 229, 100, 0.2); | 216 | background: rgba(255, 229, 100, 0.2); |
217 | display: inline-block; | ||
191 | } | 218 | } |
192 | 219 | ||
193 | .problem-abstract { | 220 | .problem-abstract { |
diff --git a/language-web/src/main/java/org/eclipse/viatra/solver/language/web/CacheControlFilter.java b/language-web/src/main/java/org/eclipse/viatra/solver/language/web/CacheControlFilter.java new file mode 100644 index 00000000..41b8e5bf --- /dev/null +++ b/language-web/src/main/java/org/eclipse/viatra/solver/language/web/CacheControlFilter.java | |||
@@ -0,0 +1,55 @@ | |||
1 | package org.eclipse.viatra.solver.language.web; | ||
2 | |||
3 | import java.io.IOException; | ||
4 | import java.util.regex.Pattern; | ||
5 | |||
6 | import javax.servlet.Filter; | ||
7 | import javax.servlet.FilterChain; | ||
8 | import javax.servlet.FilterConfig; | ||
9 | import javax.servlet.ServletException; | ||
10 | import javax.servlet.ServletRequest; | ||
11 | import javax.servlet.ServletResponse; | ||
12 | import javax.servlet.http.HttpServletRequest; | ||
13 | import javax.servlet.http.HttpServletResponse; | ||
14 | |||
15 | public class CacheControlFilter implements Filter { | ||
16 | |||
17 | private static final String CACHE_CONTROL_HEADER = "Cache-Control"; | ||
18 | |||
19 | private static final String EXPIRES_HEADER = "Expires"; | ||
20 | |||
21 | private static final Pattern CACHE_URI_PATTERN = Pattern.compile(".*\\.(css|gif|js|map|png|svg|woff2)"); | ||
22 | |||
23 | private static final long EXPIRY = 31536000; | ||
24 | |||
25 | private static final String CACHE_CONTROL_CACHE_VALUE = "public, max-age: " + EXPIRY + ", immutable"; | ||
26 | |||
27 | private static final String CACHE_CONTROL_NO_CACHE_VALUE = "no-cache, no-store, max-age: 0, must-revalidate"; | ||
28 | |||
29 | @Override | ||
30 | public void init(FilterConfig filterConfig) throws ServletException { | ||
31 | // Nothing to initialize. | ||
32 | } | ||
33 | |||
34 | @Override | ||
35 | public void doFilter(ServletRequest request, ServletResponse response, FilterChain chain) | ||
36 | throws IOException, ServletException { | ||
37 | if (request instanceof HttpServletRequest && response instanceof HttpServletResponse) { | ||
38 | var httpRequest = (HttpServletRequest) request; | ||
39 | var httpResponse = (HttpServletResponse) response; | ||
40 | if (CACHE_URI_PATTERN.matcher(httpRequest.getRequestURI()).matches()) { | ||
41 | httpResponse.setHeader(CACHE_CONTROL_HEADER, CACHE_CONTROL_CACHE_VALUE); | ||
42 | httpResponse.setDateHeader(EXPIRES_HEADER, System.currentTimeMillis() + EXPIRY * 1000L); | ||
43 | } else { | ||
44 | httpResponse.setHeader(CACHE_CONTROL_HEADER, CACHE_CONTROL_NO_CACHE_VALUE); | ||
45 | httpResponse.setDateHeader(EXPIRES_HEADER, 0); | ||
46 | } | ||
47 | } | ||
48 | chain.doFilter(request, response); | ||
49 | } | ||
50 | |||
51 | @Override | ||
52 | public void destroy() { | ||
53 | // Nothing to dispose. | ||
54 | } | ||
55 | } | ||
diff --git a/language-web/src/main/java/org/eclipse/viatra/solver/language/web/ServerLauncher.java b/language-web/src/main/java/org/eclipse/viatra/solver/language/web/ServerLauncher.java index d92c7735..a6d58f95 100644 --- a/language-web/src/main/java/org/eclipse/viatra/solver/language/web/ServerLauncher.java +++ b/language-web/src/main/java/org/eclipse/viatra/solver/language/web/ServerLauncher.java | |||
@@ -8,8 +8,10 @@ import java.io.IOException; | |||
8 | import java.net.InetSocketAddress; | 8 | import java.net.InetSocketAddress; |
9 | import java.net.URI; | 9 | import java.net.URI; |
10 | import java.net.URISyntaxException; | 10 | import java.net.URISyntaxException; |
11 | import java.util.EnumSet; | ||
11 | import java.util.Set; | 12 | import java.util.Set; |
12 | 13 | ||
14 | import javax.servlet.DispatcherType; | ||
13 | import javax.servlet.SessionTrackingMode; | 15 | import javax.servlet.SessionTrackingMode; |
14 | 16 | ||
15 | import org.eclipse.jetty.server.Server; | 17 | import org.eclipse.jetty.server.Server; |
@@ -42,6 +44,7 @@ public class ServerLauncher { | |||
42 | handler.setWelcomeFiles(new String[] { "index.html" }); | 44 | handler.setWelcomeFiles(new String[] { "index.html" }); |
43 | addDefaultServlet(handler); | 45 | addDefaultServlet(handler); |
44 | } | 46 | } |
47 | handler.addFilter(CacheControlFilter.class, "/*", EnumSet.of(DispatcherType.REQUEST)); | ||
45 | server.setHandler(handler); | 48 | server.setHandler(handler); |
46 | } | 49 | } |
47 | 50 | ||
diff --git a/language-web/src/main/js/App.tsx b/language-web/src/main/js/App.tsx index 17d4f339..5cd157fa 100644 --- a/language-web/src/main/js/App.tsx +++ b/language-web/src/main/js/App.tsx | |||
@@ -9,12 +9,12 @@ import MenuIcon from '@material-ui/icons/Menu'; | |||
9 | import PlayArrowIcon from '@material-ui/icons/PlayArrow'; | 9 | import PlayArrowIcon from '@material-ui/icons/PlayArrow'; |
10 | 10 | ||
11 | import { makeStyles } from './makeStyles'; | 11 | import { makeStyles } from './makeStyles'; |
12 | import { Editor } from './editor/Editor'; | 12 | import { EditorArea } from './editor/EditorArea'; |
13 | import { EditorButtons } from './editor/EditorButtons'; | 13 | import { EditorButtons } from './editor/EditorButtons'; |
14 | 14 | ||
15 | const useStyles = makeStyles()((theme) => ({ | 15 | const useStyles = makeStyles()((theme) => ({ |
16 | container: { | 16 | container: { |
17 | maxHeight: '100vh', | 17 | height: '100vh', |
18 | }, | 18 | }, |
19 | menuButton: { | 19 | menuButton: { |
20 | marginRight: theme.spacing(2), | 20 | marginRight: theme.spacing(2), |
@@ -85,7 +85,7 @@ export const App = (): JSX.Element => { | |||
85 | flexShrink={1} | 85 | flexShrink={1} |
86 | className={cx(classes.editorBox)} | 86 | className={cx(classes.editorBox)} |
87 | > | 87 | > |
88 | <Editor /> | 88 | <EditorArea /> |
89 | </Box> | 89 | </Box> |
90 | </Box> | 90 | </Box> |
91 | ); | 91 | ); |
diff --git a/language-web/src/main/js/editor/Editor.tsx b/language-web/src/main/js/editor/Editor.tsx deleted file mode 100644 index 9badb6a3..00000000 --- a/language-web/src/main/js/editor/Editor.tsx +++ /dev/null | |||
@@ -1,20 +0,0 @@ | |||
1 | import { observer } from 'mobx-react-lite'; | ||
2 | import React from 'react'; | ||
3 | import { Controlled as CodeMirror } from 'react-codemirror2'; | ||
4 | |||
5 | import { useRootStore } from '../RootStore'; | ||
6 | |||
7 | export const Editor = observer(() => { | ||
8 | const { editorStore } = useRootStore(); | ||
9 | |||
10 | return ( | ||
11 | <CodeMirror | ||
12 | value={editorStore.value} | ||
13 | options={editorStore.codeMirrorOptions} | ||
14 | editorDidMount={(editor) => editorStore.editorDidMount(editor)} | ||
15 | editorWillUnmount={() => editorStore.editorWillUnmount()} | ||
16 | onBeforeChange={(_editor, _data, value) => editorStore.updateValue(value)} | ||
17 | onChange={() => editorStore.reportChanged()} | ||
18 | /> | ||
19 | ); | ||
20 | }); | ||
diff --git a/language-web/src/main/js/editor/EditorArea.tsx b/language-web/src/main/js/editor/EditorArea.tsx new file mode 100644 index 00000000..f07a0ad8 --- /dev/null +++ b/language-web/src/main/js/editor/EditorArea.tsx | |||
@@ -0,0 +1,42 @@ | |||
1 | import { observer } from 'mobx-react-lite'; | ||
2 | import React, { useRef } from 'react'; | ||
3 | |||
4 | import { useRootStore } from '../RootStore'; | ||
5 | |||
6 | export const EditorArea = observer(() => { | ||
7 | const { editorStore } = useRootStore(); | ||
8 | const { CodeMirror } = editorStore.chunk || {}; | ||
9 | const fallbackTextarea = useRef<HTMLTextAreaElement>(null); | ||
10 | |||
11 | if (!CodeMirror) { | ||
12 | return ( | ||
13 | <textarea | ||
14 | value={editorStore.value} | ||
15 | onChange={(e) => editorStore.updateValue(e.target.value)} | ||
16 | ref={fallbackTextarea} | ||
17 | className={`problem-fallback-editor cm-s-${editorStore.codeMirrorTheme}`} | ||
18 | > | ||
19 | </textarea> | ||
20 | ); | ||
21 | } | ||
22 | |||
23 | const textarea = fallbackTextarea.current; | ||
24 | if (textarea) { | ||
25 | editorStore.setInitialSelection( | ||
26 | textarea.selectionStart, | ||
27 | textarea.selectionEnd, | ||
28 | document.activeElement === textarea, | ||
29 | ); | ||
30 | } | ||
31 | |||
32 | return ( | ||
33 | <CodeMirror | ||
34 | value={editorStore.value} | ||
35 | options={editorStore.codeMirrorOptions} | ||
36 | editorDidMount={(editor) => editorStore.editorDidMount(editor)} | ||
37 | editorWillUnmount={() => editorStore.editorWillUnmount()} | ||
38 | onBeforeChange={(_editor, _data, value) => editorStore.updateValue(value)} | ||
39 | onChange={() => editorStore.reportChanged()} | ||
40 | /> | ||
41 | ); | ||
42 | }); | ||
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts index 5da45ac1..1ac2e79f 100644 --- a/language-web/src/main/js/editor/EditorStore.ts +++ b/language-web/src/main/js/editor/EditorStore.ts | |||
@@ -1,19 +1,14 @@ | |||
1 | import { Editor, EditorConfiguration } from 'codemirror'; | 1 | import type { Editor, EditorConfiguration } from 'codemirror'; |
2 | import 'codemirror/addon/selection/active-line'; | ||
3 | import { | 2 | import { |
4 | createAtom, | 3 | createAtom, |
5 | makeAutoObservable, | 4 | makeAutoObservable, |
6 | observable, | 5 | observable, |
6 | runInAction, | ||
7 | } from 'mobx'; | 7 | } from 'mobx'; |
8 | import 'mode-problem'; | 8 | import type { IXtextOptions, IXtextServices } from 'xtext/xtext-codemirror'; |
9 | import { | ||
10 | IXtextOptions, | ||
11 | IXtextServices, | ||
12 | createServices, | ||
13 | removeServices, | ||
14 | } from 'xtext/xtext-codemirror'; | ||
15 | 9 | ||
16 | import { ThemeStore } from '../theme/ThemeStore'; | 10 | import type { IEditorChunk } from './editor'; |
11 | import type { ThemeStore } from '../theme/ThemeStore'; | ||
17 | 12 | ||
18 | const xtextLang = 'problem'; | 13 | const xtextLang = 'problem'; |
19 | 14 | ||
@@ -33,6 +28,8 @@ export class EditorStore { | |||
33 | 28 | ||
34 | atom; | 29 | atom; |
35 | 30 | ||
31 | chunk?: IEditorChunk; | ||
32 | |||
36 | editor?: Editor; | 33 | editor?: Editor; |
37 | 34 | ||
38 | xtextServices?: IXtextServices; | 35 | xtextServices?: IXtextServices; |
@@ -41,15 +38,56 @@ export class EditorStore { | |||
41 | 38 | ||
42 | showLineNumbers = false; | 39 | showLineNumbers = false; |
43 | 40 | ||
41 | initialSelection!: { start: number, end: number, focused: boolean }; | ||
42 | |||
44 | constructor(themeStore: ThemeStore) { | 43 | constructor(themeStore: ThemeStore) { |
45 | this.themeStore = themeStore; | 44 | this.themeStore = themeStore; |
46 | this.atom = createAtom('EditorStore'); | 45 | this.atom = createAtom('EditorStore'); |
46 | this.resetInitialSelection(); | ||
47 | makeAutoObservable(this, { | 47 | makeAutoObservable(this, { |
48 | themeStore: false, | 48 | themeStore: false, |
49 | atom: false, | 49 | atom: false, |
50 | chunk: observable.ref, | ||
50 | editor: observable.ref, | 51 | editor: observable.ref, |
51 | xtextServices: observable.ref, | 52 | xtextServices: observable.ref, |
53 | initialSelection: false, | ||
52 | }); | 54 | }); |
55 | import('./editor').then(({ editorChunk }) => { | ||
56 | runInAction(() => { | ||
57 | this.chunk = editorChunk; | ||
58 | }); | ||
59 | }).catch((error) => { | ||
60 | console.warn('Error while loading editor', error); | ||
61 | }); | ||
62 | } | ||
63 | |||
64 | setInitialSelection(start: number, end: number, focused: boolean): void { | ||
65 | this.initialSelection = { start, end, focused }; | ||
66 | this.applyInitialSelectionToEditor(); | ||
67 | } | ||
68 | |||
69 | private resetInitialSelection(): void { | ||
70 | this.initialSelection = { | ||
71 | start: 0, | ||
72 | end: 0, | ||
73 | focused: false, | ||
74 | }; | ||
75 | } | ||
76 | |||
77 | private applyInitialSelectionToEditor(): void { | ||
78 | if (this.editor) { | ||
79 | const { start, end, focused } = this.initialSelection; | ||
80 | const doc = this.editor.getDoc(); | ||
81 | const startPos = doc.posFromIndex(start); | ||
82 | const endPos = doc.posFromIndex(end); | ||
83 | doc.setSelection(startPos, endPos, { | ||
84 | scroll: true, | ||
85 | }); | ||
86 | if (focused) { | ||
87 | this.editor.focus(); | ||
88 | } | ||
89 | this.resetInitialSelection(); | ||
90 | } | ||
53 | } | 91 | } |
54 | 92 | ||
55 | /** | 93 | /** |
@@ -61,16 +99,23 @@ export class EditorStore { | |||
61 | * @param newEditor The new CodeMirror instance | 99 | * @param newEditor The new CodeMirror instance |
62 | */ | 100 | */ |
63 | editorDidMount(newEditor: Editor): void { | 101 | editorDidMount(newEditor: Editor): void { |
102 | if (!this.chunk) { | ||
103 | throw new Error('Editor not loaded yet'); | ||
104 | } | ||
64 | if (this.editor) { | 105 | if (this.editor) { |
65 | throw new Error('CoreMirror editor mounted before unmounting'); | 106 | throw new Error('CoreMirror editor mounted before unmounting'); |
66 | } | 107 | } |
67 | this.editor = newEditor; | 108 | this.editor = newEditor; |
68 | this.xtextServices = createServices(newEditor, xtextOptions); | 109 | this.xtextServices = this.chunk.createServices(newEditor, xtextOptions); |
110 | this.applyInitialSelectionToEditor(); | ||
69 | } | 111 | } |
70 | 112 | ||
71 | editorWillUnmount(): void { | 113 | editorWillUnmount(): void { |
114 | if (!this.chunk) { | ||
115 | throw new Error('Editor not loaded yet'); | ||
116 | } | ||
72 | if (this.editor) { | 117 | if (this.editor) { |
73 | removeServices(this.editor); | 118 | this.chunk.removeServices(this.editor); |
74 | } | 119 | } |
75 | delete this.editor; | 120 | delete this.editor; |
76 | delete this.xtextServices; | 121 | delete this.xtextServices; |
@@ -93,10 +138,14 @@ export class EditorStore { | |||
93 | this.atom.reportObserved(); | 138 | this.atom.reportObserved(); |
94 | } | 139 | } |
95 | 140 | ||
141 | get codeMirrorTheme(): string { | ||
142 | return `problem-${this.themeStore.className}`; | ||
143 | } | ||
144 | |||
96 | get codeMirrorOptions(): EditorConfiguration { | 145 | get codeMirrorOptions(): EditorConfiguration { |
97 | return { | 146 | return { |
98 | ...codeMirrorGlobalOptions, | 147 | ...codeMirrorGlobalOptions, |
99 | theme: this.themeStore.codeMirrorTheme, | 148 | theme: this.codeMirrorTheme, |
100 | lineNumbers: this.showLineNumbers, | 149 | lineNumbers: this.showLineNumbers, |
101 | }; | 150 | }; |
102 | } | 151 | } |
diff --git a/language-web/src/main/js/editor/editor.ts b/language-web/src/main/js/editor/editor.ts new file mode 100644 index 00000000..fbf8796b --- /dev/null +++ b/language-web/src/main/js/editor/editor.ts | |||
@@ -0,0 +1,18 @@ | |||
1 | import 'codemirror/addon/selection/active-line'; | ||
2 | import 'mode-problem'; | ||
3 | import { Controlled } from 'react-codemirror2'; | ||
4 | import { createServices, removeServices } from 'xtext/xtext-codemirror'; | ||
5 | |||
6 | export interface IEditorChunk { | ||
7 | CodeMirror: typeof Controlled; | ||
8 | |||
9 | createServices: typeof createServices; | ||
10 | |||
11 | removeServices: typeof removeServices; | ||
12 | } | ||
13 | |||
14 | export const editorChunk: IEditorChunk = { | ||
15 | CodeMirror: Controlled, | ||
16 | createServices, | ||
17 | removeServices, | ||
18 | }; | ||
diff --git a/language-web/src/main/js/theme/ThemeStore.ts b/language-web/src/main/js/theme/ThemeStore.ts index 0e4aeb23..2644a96a 100644 --- a/language-web/src/main/js/theme/ThemeStore.ts +++ b/language-web/src/main/js/theme/ThemeStore.ts | |||
@@ -51,7 +51,7 @@ export class ThemeStore { | |||
51 | return responsiveFontSizes(materialUiTheme); | 51 | return responsiveFontSizes(materialUiTheme); |
52 | } | 52 | } |
53 | 53 | ||
54 | get codeMirrorTheme(): string { | 54 | get className(): string { |
55 | return `problem-${this.currentThemeData.className}`; | 55 | return this.currentThemeData.className; |
56 | } | 56 | } |
57 | } | 57 | } |