diff options
Diffstat (limited to 'language-web')
-rw-r--r-- | language-web/package.json | 6 | ||||
-rw-r--r-- | language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java | 2 | ||||
-rw-r--r-- | language-web/src/main/js/editor/EditorStore.ts | 5 | ||||
-rw-r--r-- | language-web/src/main/js/editor/PendingRequest.ts | 47 | ||||
-rw-r--r-- | language-web/src/main/js/editor/XtextClient.ts | 243 | ||||
-rw-r--r-- | language-web/src/main/js/editor/XtextWebSocketClient.ts | 185 | ||||
-rw-r--r-- | language-web/src/main/js/editor/xtextMessages.ts | 55 | ||||
-rw-r--r-- | language-web/src/main/js/editor/xtextServiceResults.ts | 61 | ||||
-rw-r--r-- | language-web/src/main/js/index.tsx | 2 | ||||
-rw-r--r-- | language-web/webpack.config.js | 5 | ||||
-rw-r--r-- | language-web/yarn.lock | 10 |
11 files changed, 609 insertions, 12 deletions
diff --git a/language-web/package.json b/language-web/package.json index 78b080ee..016d9dc1 100644 --- a/language-web/package.json +++ b/language-web/package.json | |||
@@ -84,13 +84,13 @@ | |||
84 | "@fontsource/jetbrains-mono": "^4.5.0", | 84 | "@fontsource/jetbrains-mono": "^4.5.0", |
85 | "@fontsource/roboto": "^4.5.0", | 85 | "@fontsource/roboto": "^4.5.0", |
86 | "@lezer/lr": "^0.15.4", | 86 | "@lezer/lr": "^0.15.4", |
87 | "@mui/material": "5.0.2", | ||
88 | "@mui/icons-material": "5.0.1", | ||
89 | "jquery": "^3.6.0", | ||
90 | "loglevel": "^1.7.1", | 87 | "loglevel": "^1.7.1", |
91 | "loglevel-plugin-prefix": "^0.8.4", | 88 | "loglevel-plugin-prefix": "^0.8.4", |
89 | "@mui/material": "5.0.2", | ||
90 | "@mui/icons-material": "5.0.1", | ||
92 | "mobx": "^6.3.3", | 91 | "mobx": "^6.3.3", |
93 | "mobx-react-lite": "^3.2.1", | 92 | "mobx-react-lite": "^3.2.1", |
93 | "nanoid": "^3.1.30", | ||
94 | "react": "^17.0.2", | 94 | "react": "^17.0.2", |
95 | "react-dom": "^17.0.2" | 95 | "react-dom": "^17.0.2" |
96 | } | 96 | } |
diff --git a/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java b/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java index a8b4e123..fd41f213 100644 --- a/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java +++ b/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java | |||
@@ -61,7 +61,7 @@ public class XtextWebSocket implements WriteCallback, ResponseHandler { | |||
61 | if (webSocketSession == null) { | 61 | if (webSocketSession == null) { |
62 | return; | 62 | return; |
63 | } | 63 | } |
64 | if (statusCode == StatusCode.NORMAL) { | 64 | if (statusCode == StatusCode.NORMAL || statusCode == StatusCode.SHUTDOWN) { |
65 | LOG.debug("{} closed connection normally: {}", webSocketSession.getRemoteAddress(), reason); | 65 | LOG.debug("{} closed connection normally: {}", webSocketSession.getRemoteAddress(), reason); |
66 | } else { | 66 | } else { |
67 | LOG.warn("{} closed connection with status code {}: {}", webSocketSession.getRemoteAddress(), statusCode, | 67 | LOG.warn("{} closed connection with status code {}: {}", webSocketSession.getRemoteAddress(), statusCode, |
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts index eb358338..31bb0a11 100644 --- a/language-web/src/main/js/editor/EditorStore.ts +++ b/language-web/src/main/js/editor/EditorStore.ts | |||
@@ -41,6 +41,7 @@ import { | |||
41 | import { getLogger } from '../logging'; | 41 | import { getLogger } from '../logging'; |
42 | import { problemLanguageSupport } from './problemLanguageSupport'; | 42 | import { problemLanguageSupport } from './problemLanguageSupport'; |
43 | import type { ThemeStore } from '../theme/ThemeStore'; | 43 | import type { ThemeStore } from '../theme/ThemeStore'; |
44 | import { XtextClient } from './XtextClient'; | ||
44 | 45 | ||
45 | const log = getLogger('EditorStore'); | 46 | const log = getLogger('EditorStore'); |
46 | 47 | ||
@@ -49,7 +50,7 @@ export class EditorStore { | |||
49 | 50 | ||
50 | state: EditorState; | 51 | state: EditorState; |
51 | 52 | ||
52 | emptyHistory: unknown; | 53 | client: XtextClient; |
53 | 54 | ||
54 | showLineNumbers = false; | 55 | showLineNumbers = false; |
55 | 56 | ||
@@ -109,6 +110,7 @@ export class EditorStore { | |||
109 | problemLanguageSupport(), | 110 | problemLanguageSupport(), |
110 | ], | 111 | ], |
111 | }); | 112 | }); |
113 | this.client = new XtextClient(this); | ||
112 | reaction( | 114 | reaction( |
113 | () => this.themeStore.darkMode, | 115 | () => this.themeStore.darkMode, |
114 | (darkMode) => { | 116 | (darkMode) => { |
@@ -137,6 +139,7 @@ export class EditorStore { | |||
137 | onTransaction(tr: Transaction): void { | 139 | onTransaction(tr: Transaction): void { |
138 | log.trace('Editor transaction', tr); | 140 | log.trace('Editor transaction', tr); |
139 | this.state = tr.state; | 141 | this.state = tr.state; |
142 | this.client.onTransaction(tr); | ||
140 | } | 143 | } |
141 | 144 | ||
142 | dispatch(...specs: readonly TransactionSpec[]): void { | 145 | dispatch(...specs: readonly TransactionSpec[]): void { |
diff --git a/language-web/src/main/js/editor/PendingRequest.ts b/language-web/src/main/js/editor/PendingRequest.ts new file mode 100644 index 00000000..784f06ec --- /dev/null +++ b/language-web/src/main/js/editor/PendingRequest.ts | |||
@@ -0,0 +1,47 @@ | |||
1 | import { getLogger } from '../logging'; | ||
2 | |||
3 | const REQUEST_TIMEOUT_MS = 1000; | ||
4 | |||
5 | const log = getLogger('PendingRequest'); | ||
6 | |||
7 | export class PendingRequest { | ||
8 | private readonly resolveCallback: (value: unknown) => void; | ||
9 | |||
10 | private readonly rejectCallback: (reason?: unknown) => void; | ||
11 | |||
12 | private resolved = false; | ||
13 | |||
14 | private timeoutId: NodeJS.Timeout; | ||
15 | |||
16 | constructor(resolve: (value: unknown) => void, reject: (reason?: unknown) => void) { | ||
17 | this.resolveCallback = resolve; | ||
18 | this.rejectCallback = reject; | ||
19 | this.timeoutId = setTimeout(() => { | ||
20 | if (!this.resolved) { | ||
21 | this.reject(new Error('Request timed out')); | ||
22 | } | ||
23 | }, REQUEST_TIMEOUT_MS); | ||
24 | } | ||
25 | |||
26 | resolve(value: unknown): void { | ||
27 | if (this.resolved) { | ||
28 | log.warn('Trying to resolve already resolved promise'); | ||
29 | return; | ||
30 | } | ||
31 | this.markResolved(); | ||
32 | this.resolveCallback(value); | ||
33 | } | ||
34 | |||
35 | reject(reason?: unknown): void { | ||
36 | if (this.resolved) { | ||
37 | log.warn('Trying to reject already resolved promise'); | ||
38 | } | ||
39 | this.markResolved(); | ||
40 | this.rejectCallback(reason); | ||
41 | } | ||
42 | |||
43 | private markResolved() { | ||
44 | this.resolved = true; | ||
45 | clearTimeout(this.timeoutId); | ||
46 | } | ||
47 | } | ||
diff --git a/language-web/src/main/js/editor/XtextClient.ts b/language-web/src/main/js/editor/XtextClient.ts new file mode 100644 index 00000000..eeb67d72 --- /dev/null +++ b/language-web/src/main/js/editor/XtextClient.ts | |||
@@ -0,0 +1,243 @@ | |||
1 | import { Diagnostic, setDiagnostics } from '@codemirror/lint'; | ||
2 | import { | ||
3 | ChangeDesc, | ||
4 | ChangeSet, | ||
5 | EditorState, | ||
6 | Transaction, | ||
7 | } from '@codemirror/state'; | ||
8 | import { nanoid } from 'nanoid'; | ||
9 | |||
10 | import type { EditorStore } from './EditorStore'; | ||
11 | import { getLogger } from '../logging'; | ||
12 | import { | ||
13 | isDocumentStateResult, | ||
14 | isServiceConflictResult, | ||
15 | isValidationResult, | ||
16 | } from './xtextServiceResults'; | ||
17 | import { XtextWebSocketClient } from './XtextWebSocketClient'; | ||
18 | |||
19 | const UPDATE_TIMEOUT_MS = 300; | ||
20 | |||
21 | const log = getLogger('XtextClient'); | ||
22 | |||
23 | enum UpdateAction { | ||
24 | ForceReconnect, | ||
25 | |||
26 | FullTextUpdate, | ||
27 | } | ||
28 | |||
29 | export class XtextClient { | ||
30 | resourceName: string; | ||
31 | |||
32 | webSocketClient: XtextWebSocketClient; | ||
33 | |||
34 | xtextStateId: string | null = null; | ||
35 | |||
36 | pendingUpdate: ChangeDesc | null; | ||
37 | |||
38 | dirtyChanges: ChangeDesc; | ||
39 | |||
40 | updateTimeout: NodeJS.Timeout | null = null; | ||
41 | |||
42 | store: EditorStore; | ||
43 | |||
44 | constructor(store: EditorStore) { | ||
45 | this.resourceName = `${nanoid(7)}.problem`; | ||
46 | this.pendingUpdate = null; | ||
47 | this.store = store; | ||
48 | this.dirtyChanges = this.newEmptyChangeDesc(); | ||
49 | this.webSocketClient = new XtextWebSocketClient( | ||
50 | () => { | ||
51 | this.updateFullText().catch((error) => { | ||
52 | log.error('Unexpected error during initial update', error); | ||
53 | }); | ||
54 | }, | ||
55 | (resource, stateId, service, push) => { | ||
56 | this.onPush(resource, stateId, service, push).catch((error) => { | ||
57 | log.error('Unexected error during push message handling', error); | ||
58 | }); | ||
59 | }, | ||
60 | ); | ||
61 | } | ||
62 | |||
63 | onTransaction(transaction: Transaction): void { | ||
64 | const { changes } = transaction; | ||
65 | if (!changes.empty) { | ||
66 | this.dirtyChanges = this.dirtyChanges.composeDesc(changes.desc); | ||
67 | this.scheduleUpdate(); | ||
68 | } | ||
69 | } | ||
70 | |||
71 | private async onPush(resource: string, stateId: string, service: string, push: unknown) { | ||
72 | if (resource !== this.resourceName) { | ||
73 | log.error('Unknown resource name: expected:', this.resourceName, 'got:', resource); | ||
74 | return; | ||
75 | } | ||
76 | if (stateId !== this.xtextStateId) { | ||
77 | log.error('Unexpected xtext state id: expected:', this.xtextStateId, 'got:', resource); | ||
78 | await this.updateFullText(); | ||
79 | } | ||
80 | switch (service) { | ||
81 | case 'validate': | ||
82 | this.onValidate(push); | ||
83 | return; | ||
84 | case 'highlight': | ||
85 | // TODO | ||
86 | return; | ||
87 | default: | ||
88 | log.error('Unknown push service:', service); | ||
89 | break; | ||
90 | } | ||
91 | } | ||
92 | |||
93 | private onValidate(push: unknown) { | ||
94 | if (!isValidationResult(push)) { | ||
95 | log.error('Invalid validation result', push); | ||
96 | return; | ||
97 | } | ||
98 | const allChanges = this.computeChangesSinceLastUpdate(); | ||
99 | const diagnostics: Diagnostic[] = []; | ||
100 | push.issues.forEach((issue) => { | ||
101 | if (issue.severity === 'ignore') { | ||
102 | return; | ||
103 | } | ||
104 | diagnostics.push({ | ||
105 | from: allChanges.mapPos(issue.offset), | ||
106 | to: allChanges.mapPos(issue.offset + issue.length), | ||
107 | severity: issue.severity, | ||
108 | message: issue.description, | ||
109 | }); | ||
110 | }); | ||
111 | this.store.dispatch(setDiagnostics(this.store.state, diagnostics)); | ||
112 | } | ||
113 | |||
114 | private computeChangesSinceLastUpdate() { | ||
115 | if (this.pendingUpdate === null) { | ||
116 | return this.dirtyChanges; | ||
117 | } | ||
118 | return this.pendingUpdate.composeDesc(this.dirtyChanges); | ||
119 | } | ||
120 | |||
121 | private scheduleUpdate() { | ||
122 | if (this.updateTimeout !== null) { | ||
123 | clearTimeout(this.updateTimeout); | ||
124 | } | ||
125 | this.updateTimeout = setTimeout(() => { | ||
126 | this.updateTimeout = null; | ||
127 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { | ||
128 | return; | ||
129 | } | ||
130 | if (!this.pendingUpdate) { | ||
131 | this.updateDeltaText().catch((error) => { | ||
132 | log.error('Unexpected error during scheduled update', error); | ||
133 | }); | ||
134 | } | ||
135 | this.scheduleUpdate(); | ||
136 | }, UPDATE_TIMEOUT_MS); | ||
137 | } | ||
138 | |||
139 | private newEmptyChangeDesc() { | ||
140 | const changeSet = ChangeSet.of([], this.store.state.doc.length); | ||
141 | return changeSet.desc; | ||
142 | } | ||
143 | |||
144 | private async updateFullText() { | ||
145 | await this.withUpdate(async () => { | ||
146 | const result = await this.webSocketClient.send({ | ||
147 | resource: this.resourceName, | ||
148 | serviceType: 'update', | ||
149 | fullText: this.store.state.doc.sliceString(0), | ||
150 | }); | ||
151 | if (isDocumentStateResult(result)) { | ||
152 | return result.stateId; | ||
153 | } | ||
154 | if (isServiceConflictResult(result)) { | ||
155 | log.error('Full text update conflict:', result.conflict); | ||
156 | if (result.conflict === 'canceled') { | ||
157 | return UpdateAction.FullTextUpdate; | ||
158 | } | ||
159 | return UpdateAction.ForceReconnect; | ||
160 | } | ||
161 | log.error('Unexpected full text update result:', result); | ||
162 | return UpdateAction.ForceReconnect; | ||
163 | }); | ||
164 | } | ||
165 | |||
166 | private async updateDeltaText() { | ||
167 | if (this.xtextStateId === null) { | ||
168 | await this.updateFullText(); | ||
169 | return; | ||
170 | } | ||
171 | const delta = this.computeDelta(); | ||
172 | log.debug('Editor delta', delta); | ||
173 | await this.withUpdate(async () => { | ||
174 | const result = await this.webSocketClient.send({ | ||
175 | resource: this.resourceName, | ||
176 | serviceType: 'update', | ||
177 | requiredStateId: this.xtextStateId, | ||
178 | ...delta, | ||
179 | }); | ||
180 | if (isDocumentStateResult(result)) { | ||
181 | return result.stateId; | ||
182 | } | ||
183 | if (isServiceConflictResult(result)) { | ||
184 | log.error('Delta text update conflict:', result.conflict); | ||
185 | return UpdateAction.FullTextUpdate; | ||
186 | } | ||
187 | log.error('Unexpected delta text update result:', result); | ||
188 | return UpdateAction.ForceReconnect; | ||
189 | }); | ||
190 | } | ||
191 | |||
192 | private computeDelta() { | ||
193 | if (this.dirtyChanges.empty) { | ||
194 | return {}; | ||
195 | } | ||
196 | let minFromA = Number.MAX_SAFE_INTEGER; | ||
197 | let maxToA = 0; | ||
198 | let minFromB = Number.MAX_SAFE_INTEGER; | ||
199 | let maxToB = 0; | ||
200 | this.dirtyChanges.iterChangedRanges((fromA, toA, fromB, toB) => { | ||
201 | minFromA = Math.min(minFromA, fromA); | ||
202 | maxToA = Math.max(maxToA, toA); | ||
203 | minFromB = Math.min(minFromB, fromB); | ||
204 | maxToB = Math.max(maxToB, toB); | ||
205 | }); | ||
206 | return { | ||
207 | deltaOffset: minFromA, | ||
208 | deltaReplaceLength: maxToA - minFromA, | ||
209 | deltaText: this.store.state.doc.sliceString(minFromB, maxToB), | ||
210 | }; | ||
211 | } | ||
212 | |||
213 | private async withUpdate(callback: () => Promise<string | UpdateAction>) { | ||
214 | if (this.pendingUpdate !== null) { | ||
215 | log.error('Another update is pending, will not perform update'); | ||
216 | return; | ||
217 | } | ||
218 | this.pendingUpdate = this.dirtyChanges; | ||
219 | this.dirtyChanges = this.newEmptyChangeDesc(); | ||
220 | let newStateId: string | UpdateAction = UpdateAction.ForceReconnect; | ||
221 | try { | ||
222 | newStateId = await callback(); | ||
223 | } catch (error) { | ||
224 | log.error('Error while updating state', error); | ||
225 | } finally { | ||
226 | if (typeof newStateId === 'string') { | ||
227 | this.xtextStateId = newStateId; | ||
228 | this.pendingUpdate = null; | ||
229 | } else { | ||
230 | this.dirtyChanges = this.pendingUpdate.composeDesc(this.dirtyChanges); | ||
231 | this.pendingUpdate = null; | ||
232 | switch (newStateId) { | ||
233 | case UpdateAction.ForceReconnect: | ||
234 | this.webSocketClient.forceReconnectDueToError(); | ||
235 | break; | ||
236 | case UpdateAction.FullTextUpdate: | ||
237 | await this.updateFullText(); | ||
238 | break; | ||
239 | } | ||
240 | } | ||
241 | } | ||
242 | } | ||
243 | } | ||
diff --git a/language-web/src/main/js/editor/XtextWebSocketClient.ts b/language-web/src/main/js/editor/XtextWebSocketClient.ts new file mode 100644 index 00000000..131e0067 --- /dev/null +++ b/language-web/src/main/js/editor/XtextWebSocketClient.ts | |||
@@ -0,0 +1,185 @@ | |||
1 | import { getLogger } from '../logging'; | ||
2 | import { PendingRequest } from './PendingRequest'; | ||
3 | import { | ||
4 | isErrorResponse, | ||
5 | isOkResponse, | ||
6 | isPushMessage, | ||
7 | IXtextWebRequest, | ||
8 | } from './xtextMessages'; | ||
9 | |||
10 | const XTEXT_SUBPROTOCOL_V1 = 'tools.refinery.language.web.xtext.v1'; | ||
11 | |||
12 | const WEBSOCKET_CLOSE_OK = 1000; | ||
13 | |||
14 | const RECONNECT_DELAY_MS = 1000; | ||
15 | |||
16 | const log = getLogger('XtextWebSocketClient'); | ||
17 | |||
18 | type ReconnectHandler = () => void; | ||
19 | |||
20 | type PushHandler = (resourceId: string, stateId: string, service: string, data: unknown) => void; | ||
21 | |||
22 | export class XtextWebSocketClient { | ||
23 | nextMessageId = 0; | ||
24 | |||
25 | closing = false; | ||
26 | |||
27 | connection!: WebSocket; | ||
28 | |||
29 | pendingRequests = new Map<string, PendingRequest>(); | ||
30 | |||
31 | onReconnect: ReconnectHandler; | ||
32 | |||
33 | onPush: PushHandler; | ||
34 | |||
35 | reconnectTimeout: NodeJS.Timeout | null = null; | ||
36 | |||
37 | constructor(onReconnect: ReconnectHandler, onPush: PushHandler) { | ||
38 | this.onReconnect = onReconnect; | ||
39 | this.onPush = onPush; | ||
40 | this.reconnect(); | ||
41 | } | ||
42 | |||
43 | get isOpen(): boolean { | ||
44 | return this.connection.readyState === WebSocket.OPEN; | ||
45 | } | ||
46 | |||
47 | private reconnect() { | ||
48 | this.reconnectTimeout = null; | ||
49 | const webSocketServer = window.origin.replace(/^http/, 'ws'); | ||
50 | const webSocketUrl = `${webSocketServer}/xtext-service`; | ||
51 | this.connection = new WebSocket(webSocketUrl, XTEXT_SUBPROTOCOL_V1); | ||
52 | this.connection.addEventListener('open', () => { | ||
53 | if (this.connection.protocol !== XTEXT_SUBPROTOCOL_V1) { | ||
54 | log.error('Unknown subprotocol', this.connection.protocol, 'selected by server'); | ||
55 | this.forceReconnectDueToError(); | ||
56 | return; | ||
57 | } | ||
58 | log.info('Connected to xtext web services'); | ||
59 | this.onReconnect(); | ||
60 | }); | ||
61 | this.connection.addEventListener('error', (event) => { | ||
62 | log.error('Unexpected websocket error', event); | ||
63 | this.forceReconnectDueToError(); | ||
64 | }); | ||
65 | this.connection.addEventListener('message', (event) => { | ||
66 | this.handleMessage(event.data); | ||
67 | }); | ||
68 | this.connection.addEventListener('close', (event) => { | ||
69 | if (!this.closing || event.code !== WEBSOCKET_CLOSE_OK) { | ||
70 | log.error('Websocket closed undexpectedly', event.code, event.reason); | ||
71 | } | ||
72 | this.cleanupAndMaybeReconnect(); | ||
73 | }); | ||
74 | } | ||
75 | |||
76 | private cleanupAndMaybeReconnect() { | ||
77 | this.pendingRequests.forEach((pendingRequest) => { | ||
78 | pendingRequest.reject(new Error('Websocket closed')); | ||
79 | }); | ||
80 | this.pendingRequests.clear(); | ||
81 | if (this.closing) { | ||
82 | return; | ||
83 | } | ||
84 | if (this.reconnectTimeout !== null) { | ||
85 | clearTimeout(this.reconnectTimeout); | ||
86 | } | ||
87 | this.reconnectTimeout = setTimeout(() => { | ||
88 | log.info('Attempting to reconnect websocket'); | ||
89 | this.reconnect(); | ||
90 | }, RECONNECT_DELAY_MS); | ||
91 | } | ||
92 | |||
93 | public forceReconnectDueToError(): void { | ||
94 | this.closeConnection(); | ||
95 | this.cleanupAndMaybeReconnect(); | ||
96 | } | ||
97 | |||
98 | send(request: unknown): Promise<unknown> { | ||
99 | if (!this.isOpen) { | ||
100 | throw new Error('Connection is not open'); | ||
101 | } | ||
102 | const messageId = this.nextMessageId.toString(16); | ||
103 | if (messageId in this.pendingRequests) { | ||
104 | log.error('Message id wraparound still pending', messageId); | ||
105 | this.rejectRequest(messageId, new Error('Message id wraparound')); | ||
106 | } | ||
107 | if (this.nextMessageId >= Number.MAX_SAFE_INTEGER) { | ||
108 | this.nextMessageId = 0; | ||
109 | } else { | ||
110 | this.nextMessageId += 1; | ||
111 | } | ||
112 | const message = JSON.stringify({ | ||
113 | id: messageId, | ||
114 | request, | ||
115 | } as IXtextWebRequest); | ||
116 | return new Promise((resolve, reject) => { | ||
117 | this.connection.send(message); | ||
118 | this.pendingRequests.set(messageId, new PendingRequest(resolve, reject)); | ||
119 | }); | ||
120 | } | ||
121 | |||
122 | private handleMessage(messageStr: unknown) { | ||
123 | if (typeof messageStr !== 'string') { | ||
124 | log.error('Unexpected binary message', messageStr); | ||
125 | this.forceReconnectDueToError(); | ||
126 | return; | ||
127 | } | ||
128 | log.trace('Incoming websocket message', messageStr); | ||
129 | let message: unknown; | ||
130 | try { | ||
131 | message = JSON.parse(messageStr); | ||
132 | } catch (error) { | ||
133 | log.error('Json parse error', error); | ||
134 | this.forceReconnectDueToError(); | ||
135 | return; | ||
136 | } | ||
137 | if (isOkResponse(message)) { | ||
138 | this.resolveRequest(message.id, message.response); | ||
139 | } else if (isErrorResponse(message)) { | ||
140 | this.rejectRequest(message.id, new Error(`${message.error} error: ${message.message}`)); | ||
141 | if (message.error === 'server') { | ||
142 | log.error('Reconnecting due to server error: ', message.message); | ||
143 | this.forceReconnectDueToError(); | ||
144 | } | ||
145 | } else if (isPushMessage(message)) { | ||
146 | this.onPush(message.resource, message.stateId, message.service, message.push); | ||
147 | } else { | ||
148 | log.error('Unexpected websocket message', message); | ||
149 | this.forceReconnectDueToError(); | ||
150 | } | ||
151 | } | ||
152 | |||
153 | private resolveRequest(messageId: string, value: unknown) { | ||
154 | const pendingRequest = this.pendingRequests.get(messageId); | ||
155 | this.pendingRequests.delete(messageId); | ||
156 | if (pendingRequest) { | ||
157 | pendingRequest.resolve(value); | ||
158 | return; | ||
159 | } | ||
160 | log.error('Trying to resolve unknown request', messageId, 'with', value); | ||
161 | } | ||
162 | |||
163 | private rejectRequest(messageId: string, reason?: unknown) { | ||
164 | const pendingRequest = this.pendingRequests.get(messageId); | ||
165 | this.pendingRequests.delete(messageId); | ||
166 | if (pendingRequest) { | ||
167 | pendingRequest.reject(reason); | ||
168 | return; | ||
169 | } | ||
170 | log.error('Trying to reject unknown request', messageId, 'with', reason); | ||
171 | } | ||
172 | |||
173 | private closeConnection() { | ||
174 | if (this.connection && this.connection.readyState !== WebSocket.CLOSING | ||
175 | && this.connection.readyState !== WebSocket.CLOSED) { | ||
176 | log.info('Closing websocket connection'); | ||
177 | this.connection.close(); | ||
178 | } | ||
179 | } | ||
180 | |||
181 | close(): void { | ||
182 | this.closing = true; | ||
183 | this.closeConnection(); | ||
184 | } | ||
185 | } | ||
diff --git a/language-web/src/main/js/editor/xtextMessages.ts b/language-web/src/main/js/editor/xtextMessages.ts new file mode 100644 index 00000000..d3cb9425 --- /dev/null +++ b/language-web/src/main/js/editor/xtextMessages.ts | |||
@@ -0,0 +1,55 @@ | |||
1 | export interface IXtextWebRequest { | ||
2 | id: string; | ||
3 | |||
4 | request: unknown; | ||
5 | } | ||
6 | |||
7 | export interface IXtextWebOkResponse { | ||
8 | id: string; | ||
9 | |||
10 | response: unknown; | ||
11 | } | ||
12 | |||
13 | export function isOkResponse(response: unknown): response is IXtextWebOkResponse { | ||
14 | const okResponse = response as IXtextWebOkResponse; | ||
15 | return typeof okResponse.id === 'string' | ||
16 | && typeof okResponse.response !== 'undefined'; | ||
17 | } | ||
18 | |||
19 | export const VALID_XTEXT_WEB_ERROR_KINDS = ['request', 'server'] as const; | ||
20 | |||
21 | export type XtextWebErrorKind = typeof VALID_XTEXT_WEB_ERROR_KINDS[number]; | ||
22 | |||
23 | export interface IXtextWebErrorResponse { | ||
24 | id: string; | ||
25 | |||
26 | error: XtextWebErrorKind; | ||
27 | |||
28 | message: string; | ||
29 | } | ||
30 | |||
31 | export function isErrorResponse(response: unknown): response is IXtextWebErrorResponse { | ||
32 | const errorResponse = response as IXtextWebErrorResponse; | ||
33 | return typeof errorResponse.id === 'string' | ||
34 | && typeof errorResponse.error === 'string' | ||
35 | && VALID_XTEXT_WEB_ERROR_KINDS.includes(errorResponse.error) | ||
36 | && typeof errorResponse.message === 'string'; | ||
37 | } | ||
38 | |||
39 | export interface IXtextWebPushMessage { | ||
40 | resource: string; | ||
41 | |||
42 | stateId: string; | ||
43 | |||
44 | service: string; | ||
45 | |||
46 | push: unknown; | ||
47 | } | ||
48 | |||
49 | export function isPushMessage(response: unknown): response is IXtextWebPushMessage { | ||
50 | const pushMessage = response as IXtextWebPushMessage; | ||
51 | return typeof pushMessage.resource === 'string' | ||
52 | && typeof pushMessage.stateId === 'string' | ||
53 | && typeof pushMessage.service === 'string' | ||
54 | && typeof pushMessage.push !== 'undefined'; | ||
55 | } | ||
diff --git a/language-web/src/main/js/editor/xtextServiceResults.ts b/language-web/src/main/js/editor/xtextServiceResults.ts new file mode 100644 index 00000000..2a66566a --- /dev/null +++ b/language-web/src/main/js/editor/xtextServiceResults.ts | |||
@@ -0,0 +1,61 @@ | |||
1 | export interface IDocumentStateResult { | ||
2 | stateId: string; | ||
3 | } | ||
4 | |||
5 | export function isDocumentStateResult(result: unknown): result is IDocumentStateResult { | ||
6 | const documentStateResult = result as IDocumentStateResult; | ||
7 | return typeof documentStateResult.stateId === 'string'; | ||
8 | } | ||
9 | |||
10 | export const VALID_CONFLICTS = ['invalidStateId', 'canceled'] as const; | ||
11 | |||
12 | export type Conflict = typeof VALID_CONFLICTS[number]; | ||
13 | |||
14 | export interface IServiceConflictResult { | ||
15 | conflict: Conflict; | ||
16 | } | ||
17 | |||
18 | export function isServiceConflictResult(result: unknown): result is IServiceConflictResult { | ||
19 | const serviceConflictResult = result as IServiceConflictResult; | ||
20 | return typeof serviceConflictResult.conflict === 'string' | ||
21 | && VALID_CONFLICTS.includes(serviceConflictResult.conflict); | ||
22 | } | ||
23 | |||
24 | export const VALID_SEVERITIES = ['error', 'warning', 'info', 'ignore'] as const; | ||
25 | |||
26 | export type Severity = typeof VALID_SEVERITIES[number]; | ||
27 | |||
28 | export interface IIssue { | ||
29 | description: string; | ||
30 | |||
31 | severity: Severity; | ||
32 | |||
33 | line: number; | ||
34 | |||
35 | column: number; | ||
36 | |||
37 | offset: number; | ||
38 | |||
39 | length: number; | ||
40 | } | ||
41 | |||
42 | export function isIssue(value: unknown): value is IIssue { | ||
43 | const issue = value as IIssue; | ||
44 | return typeof issue.description === 'string' | ||
45 | && typeof issue.severity === 'string' | ||
46 | && VALID_SEVERITIES.includes(issue.severity) | ||
47 | && typeof issue.line === 'number' | ||
48 | && typeof issue.column === 'number' | ||
49 | && typeof issue.offset === 'number' | ||
50 | && typeof issue.length === 'number'; | ||
51 | } | ||
52 | |||
53 | export interface IValidationResult { | ||
54 | issues: IIssue[]; | ||
55 | } | ||
56 | |||
57 | export function isValidationResult(result: unknown): result is IValidationResult { | ||
58 | const validationResult = result as IValidationResult; | ||
59 | return Array.isArray(validationResult.issues) | ||
60 | && validationResult.issues.every(isIssue); | ||
61 | } | ||
diff --git a/language-web/src/main/js/index.tsx b/language-web/src/main/js/index.tsx index 9316db4d..1b24eadb 100644 --- a/language-web/src/main/js/index.tsx +++ b/language-web/src/main/js/index.tsx | |||
@@ -26,7 +26,7 @@ enum TaxStatus { | |||
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), | 28 | taxStatus(p, child), |
29 | children(p, _q), | 29 | children(p, _q) |
30 | ; taxStatus(p, retired), | 30 | ; taxStatus(p, retired), |
31 | parent(p, q), | 31 | parent(p, q), |
32 | !taxStatus(q, retired). | 32 | !taxStatus(q, retired). |
diff --git a/language-web/webpack.config.js b/language-web/webpack.config.js index 55b590ca..6714fa6b 100644 --- a/language-web/webpack.config.js +++ b/language-web/webpack.config.js | |||
@@ -191,7 +191,10 @@ module.exports = { | |||
191 | host: listenHost, | 191 | host: listenHost, |
192 | port: listenPort, | 192 | port: listenPort, |
193 | proxy: { | 193 | proxy: { |
194 | '/xtext-service': `${apiPort === 443 ? 'https' : 'http'}://${apiHost}:${apiPort}`, | 194 | '/xtext-service': { |
195 | target: `${apiPort === 443 ? 'https' : 'http'}://${apiHost}:${apiPort}`, | ||
196 | ws: true, | ||
197 | }, | ||
195 | }, | 198 | }, |
196 | }, | 199 | }, |
197 | plugins: [ | 200 | plugins: [ |
diff --git a/language-web/yarn.lock b/language-web/yarn.lock index 360c5be3..9d899a52 100644 --- a/language-web/yarn.lock +++ b/language-web/yarn.lock | |||
@@ -4850,11 +4850,6 @@ jest-worker@^27.0.6: | |||
4850 | merge-stream "^2.0.0" | 4850 | merge-stream "^2.0.0" |
4851 | supports-color "^8.0.0" | 4851 | supports-color "^8.0.0" |
4852 | 4852 | ||
4853 | jquery@^3.6.0: | ||
4854 | version "3.6.0" | ||
4855 | resolved "https://registry.yarnpkg.com/jquery/-/jquery-3.6.0.tgz#c72a09f15c1bdce142f49dbf1170bdf8adac2470" | ||
4856 | integrity sha512-JVzAR/AjBvVt2BmYhxRCSYysDsPcssdmTFnzyLEts9qNwmjmu4JTAMYubEfwVOSwpQ1I1sKKFcxhZCI2buerfw== | ||
4857 | |||
4858 | "js-tokens@^3.0.0 || ^4.0.0", js-tokens@^4.0.0: | 4853 | "js-tokens@^3.0.0 || ^4.0.0", js-tokens@^4.0.0: |
4859 | version "4.0.0" | 4854 | version "4.0.0" |
4860 | resolved "https://registry.yarnpkg.com/js-tokens/-/js-tokens-4.0.0.tgz#19203fb59991df98e3a287050d4647cdeaf32499" | 4855 | resolved "https://registry.yarnpkg.com/js-tokens/-/js-tokens-4.0.0.tgz#19203fb59991df98e3a287050d4647cdeaf32499" |
@@ -5456,6 +5451,11 @@ nanoid@^3.1.25: | |||
5456 | resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.1.28.tgz#3c01bac14cb6c5680569014cc65a2f26424c6bd4" | 5451 | resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.1.28.tgz#3c01bac14cb6c5680569014cc65a2f26424c6bd4" |
5457 | integrity sha512-gSu9VZ2HtmoKYe/lmyPFES5nknFrHa+/DT9muUFWFMi6Jh9E1I7bkvlQ8xxf1Kos9pi9o8lBnIOkatMhKX/YUw== | 5452 | integrity sha512-gSu9VZ2HtmoKYe/lmyPFES5nknFrHa+/DT9muUFWFMi6Jh9E1I7bkvlQ8xxf1Kos9pi9o8lBnIOkatMhKX/YUw== |
5458 | 5453 | ||
5454 | nanoid@^3.1.30: | ||
5455 | version "3.1.30" | ||
5456 | resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.1.30.tgz#63f93cc548d2a113dc5dfbc63bfa09e2b9b64362" | ||
5457 | integrity sha512-zJpuPDwOv8D2zq2WRoMe1HsfZthVewpel9CAvTfc/2mBD1uUT/agc5f7GHGWXlYkFvi1mVxe4IjvP2HNrop7nQ== | ||
5458 | |||
5459 | natural-compare@^1.4.0: | 5459 | natural-compare@^1.4.0: |
5460 | version "1.4.0" | 5460 | version "1.4.0" |
5461 | resolved "https://registry.yarnpkg.com/natural-compare/-/natural-compare-1.4.0.tgz#4abebfeed7541f2c27acfb29bdbbd15c8d5ba4f7" | 5461 | resolved "https://registry.yarnpkg.com/natural-compare/-/natural-compare-1.4.0.tgz#4abebfeed7541f2c27acfb29bdbbd15c8d5ba4f7" |