diff options
author | 2021-10-30 13:48:52 +0200 | |
---|---|---|
committer | 2021-10-31 19:26:13 +0100 | |
commit | cdb493b0a47bcf64e8e670b94fa399fcd731f531 (patch) | |
tree | b6b03aec77ef87a2dda7585be7884a30c65d93f5 /language-web/src/main/js/editor | |
parent | feat(web): add xtext content assist (diff) | |
download | refinery-cdb493b0a47bcf64e8e670b94fa399fcd731f531.tar.gz refinery-cdb493b0a47bcf64e8e670b94fa399fcd731f531.tar.zst refinery-cdb493b0a47bcf64e8e670b94fa399fcd731f531.zip |
chore(web): refactor xtext client
Diffstat (limited to 'language-web/src/main/js/editor')
-rw-r--r-- | language-web/src/main/js/editor/EditorStore.ts | 4 | ||||
-rw-r--r-- | language-web/src/main/js/editor/XtextClient.ts | 424 | ||||
-rw-r--r-- | language-web/src/main/js/editor/XtextWebSocketClient.ts | 345 | ||||
-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 | 129 | ||||
-rw-r--r-- | language-web/src/main/js/editor/problemLanguageSupport.ts | 83 | ||||
-rw-r--r-- | language-web/src/main/js/editor/xtextMessages.ts | 62 | ||||
-rw-r--r-- | language-web/src/main/js/editor/xtextServiceResults.ts | 200 |
9 files changed, 2 insertions, 1426 deletions
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts index dcc69fd1..be9295bf 100644 --- a/language-web/src/main/js/editor/EditorStore.ts +++ b/language-web/src/main/js/editor/EditorStore.ts | |||
@@ -42,10 +42,10 @@ import { | |||
42 | reaction, | 42 | reaction, |
43 | } from 'mobx'; | 43 | } from 'mobx'; |
44 | 44 | ||
45 | import { problemLanguageSupport } from '../language/problemLanguageSupport'; | ||
45 | import { getLogger } from '../logging'; | 46 | import { getLogger } from '../logging'; |
46 | import { problemLanguageSupport } from './problemLanguageSupport'; | ||
47 | import type { ThemeStore } from '../theme/ThemeStore'; | 47 | import type { ThemeStore } from '../theme/ThemeStore'; |
48 | import { XtextClient } from './XtextClient'; | 48 | import { XtextClient } from '../xtext/XtextClient'; |
49 | 49 | ||
50 | const log = getLogger('EditorStore'); | 50 | const log = getLogger('EditorStore'); |
51 | 51 | ||
diff --git a/language-web/src/main/js/editor/XtextClient.ts b/language-web/src/main/js/editor/XtextClient.ts deleted file mode 100644 index 6f789fb7..00000000 --- a/language-web/src/main/js/editor/XtextClient.ts +++ /dev/null | |||
@@ -1,424 +0,0 @@ | |||
1 | import { | ||
2 | Completion, | ||
3 | CompletionContext, | ||
4 | CompletionResult, | ||
5 | } from '@codemirror/autocomplete'; | ||
6 | import type { Diagnostic } from '@codemirror/lint'; | ||
7 | import { | ||
8 | ChangeDesc, | ||
9 | ChangeSet, | ||
10 | Transaction, | ||
11 | } from '@codemirror/state'; | ||
12 | import { nanoid } from 'nanoid'; | ||
13 | |||
14 | import type { EditorStore } from './EditorStore'; | ||
15 | import { getLogger } from '../logging'; | ||
16 | import { Timer } from '../utils/Timer'; | ||
17 | import { | ||
18 | IContentAssistEntry, | ||
19 | isContentAssistResult, | ||
20 | isDocumentStateResult, | ||
21 | isInvalidStateIdConflictResult, | ||
22 | isValidationResult, | ||
23 | } from './xtextServiceResults'; | ||
24 | import { XtextWebSocketClient } from './XtextWebSocketClient'; | ||
25 | import { PendingTask } from '../utils/PendingTask'; | ||
26 | |||
27 | const UPDATE_TIMEOUT_MS = 500; | ||
28 | |||
29 | const WAIT_FOR_UPDATE_TIMEOUT_MS = 1000; | ||
30 | |||
31 | const log = getLogger('XtextClient'); | ||
32 | |||
33 | export class XtextClient { | ||
34 | resourceName: string; | ||
35 | |||
36 | webSocketClient: XtextWebSocketClient; | ||
37 | |||
38 | xtextStateId: string | null = null; | ||
39 | |||
40 | pendingUpdate: ChangeDesc | null; | ||
41 | |||
42 | dirtyChanges: ChangeDesc; | ||
43 | |||
44 | lastCompletion: CompletionResult | null = null; | ||
45 | |||
46 | updateListeners: PendingTask<void>[] = []; | ||
47 | |||
48 | updateTimer = new Timer(() => { | ||
49 | this.handleUpdate(); | ||
50 | }, UPDATE_TIMEOUT_MS); | ||
51 | |||
52 | store: EditorStore; | ||
53 | |||
54 | constructor(store: EditorStore) { | ||
55 | this.resourceName = `${nanoid(7)}.problem`; | ||
56 | this.pendingUpdate = null; | ||
57 | this.store = store; | ||
58 | this.dirtyChanges = this.newEmptyChangeDesc(); | ||
59 | this.webSocketClient = new XtextWebSocketClient( | ||
60 | async () => { | ||
61 | this.xtextStateId = null; | ||
62 | await this.updateFullText(); | ||
63 | }, | ||
64 | async (resource, stateId, service, push) => { | ||
65 | await this.onPush(resource, stateId, service, push); | ||
66 | }, | ||
67 | ); | ||
68 | } | ||
69 | |||
70 | onTransaction(transaction: Transaction): void { | ||
71 | const { changes } = transaction; | ||
72 | if (!changes.empty) { | ||
73 | if (this.shouldInvalidateCachedCompletion(transaction)) { | ||
74 | log.trace('Invalidating cached completions'); | ||
75 | this.lastCompletion = null; | ||
76 | } | ||
77 | this.dirtyChanges = this.dirtyChanges.composeDesc(changes.desc); | ||
78 | this.updateTimer.reschedule(); | ||
79 | } | ||
80 | } | ||
81 | |||
82 | private async onPush(resource: string, stateId: string, service: string, push: unknown) { | ||
83 | if (resource !== this.resourceName) { | ||
84 | log.error('Unknown resource name: expected:', this.resourceName, 'got:', resource); | ||
85 | return; | ||
86 | } | ||
87 | if (stateId !== this.xtextStateId) { | ||
88 | log.error('Unexpected xtext state id: expected:', this.xtextStateId, 'got:', resource); | ||
89 | await this.updateFullText(); | ||
90 | } | ||
91 | switch (service) { | ||
92 | case 'validate': | ||
93 | this.onValidate(push); | ||
94 | return; | ||
95 | case 'highlight': | ||
96 | // TODO | ||
97 | return; | ||
98 | default: | ||
99 | log.error('Unknown push service:', service); | ||
100 | break; | ||
101 | } | ||
102 | } | ||
103 | |||
104 | private onValidate(push: unknown) { | ||
105 | if (!isValidationResult(push)) { | ||
106 | log.error('Invalid validation result', push); | ||
107 | return; | ||
108 | } | ||
109 | const allChanges = this.computeChangesSinceLastUpdate(); | ||
110 | const diagnostics: Diagnostic[] = []; | ||
111 | push.issues.forEach((issue) => { | ||
112 | if (issue.severity === 'ignore') { | ||
113 | return; | ||
114 | } | ||
115 | diagnostics.push({ | ||
116 | from: allChanges.mapPos(issue.offset), | ||
117 | to: allChanges.mapPos(issue.offset + issue.length), | ||
118 | severity: issue.severity, | ||
119 | message: issue.description, | ||
120 | }); | ||
121 | }); | ||
122 | this.store.updateDiagnostics(diagnostics); | ||
123 | } | ||
124 | |||
125 | private computeChangesSinceLastUpdate() { | ||
126 | return this.pendingUpdate?.composeDesc(this.dirtyChanges) || this.dirtyChanges; | ||
127 | } | ||
128 | |||
129 | private handleUpdate() { | ||
130 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { | ||
131 | return; | ||
132 | } | ||
133 | if (this.pendingUpdate === null) { | ||
134 | this.update().catch((error) => { | ||
135 | log.error('Unexpected error during scheduled update', error); | ||
136 | }); | ||
137 | } | ||
138 | this.updateTimer.reschedule(); | ||
139 | } | ||
140 | |||
141 | private newEmptyChangeDesc() { | ||
142 | const changeSet = ChangeSet.of([], this.store.state.doc.length); | ||
143 | return changeSet.desc; | ||
144 | } | ||
145 | |||
146 | private async updateFullText() { | ||
147 | await this.withUpdate(() => this.doUpdateFullText()); | ||
148 | } | ||
149 | |||
150 | private async doUpdateFullText(): Promise<[string, void]> { | ||
151 | const result = await this.webSocketClient.send({ | ||
152 | resource: this.resourceName, | ||
153 | serviceType: 'update', | ||
154 | fullText: this.store.state.doc.sliceString(0), | ||
155 | }); | ||
156 | if (isDocumentStateResult(result)) { | ||
157 | return [result.stateId, undefined]; | ||
158 | } | ||
159 | log.error('Unexpected full text update result:', result); | ||
160 | throw new Error('Full text update failed'); | ||
161 | } | ||
162 | |||
163 | async update(): Promise<void> { | ||
164 | await this.prepareForDeltaUpdate(); | ||
165 | const delta = this.computeDelta(); | ||
166 | if (delta === null) { | ||
167 | return; | ||
168 | } | ||
169 | log.trace('Editor delta', delta); | ||
170 | await this.withUpdate(async () => { | ||
171 | const result = await this.webSocketClient.send({ | ||
172 | resource: this.resourceName, | ||
173 | serviceType: 'update', | ||
174 | requiredStateId: this.xtextStateId, | ||
175 | ...delta, | ||
176 | }); | ||
177 | if (isDocumentStateResult(result)) { | ||
178 | return [result.stateId, undefined]; | ||
179 | } | ||
180 | if (isInvalidStateIdConflictResult(result)) { | ||
181 | return this.doFallbackToUpdateFullText(); | ||
182 | } | ||
183 | log.error('Unexpected delta text update result:', result); | ||
184 | throw new Error('Delta text update failed'); | ||
185 | }); | ||
186 | } | ||
187 | |||
188 | private doFallbackToUpdateFullText() { | ||
189 | if (this.pendingUpdate === null) { | ||
190 | throw new Error('Only a pending update can be extended'); | ||
191 | } | ||
192 | log.warn('Delta update failed, performing full text update'); | ||
193 | this.xtextStateId = null; | ||
194 | this.pendingUpdate = this.pendingUpdate.composeDesc(this.dirtyChanges); | ||
195 | this.dirtyChanges = this.newEmptyChangeDesc(); | ||
196 | return this.doUpdateFullText(); | ||
197 | } | ||
198 | |||
199 | async contentAssist(context: CompletionContext): Promise<CompletionResult> { | ||
200 | const tokenBefore = context.tokenBefore(['QualifiedName']); | ||
201 | if (tokenBefore === null && !context.explicit) { | ||
202 | return { | ||
203 | from: context.pos, | ||
204 | options: [], | ||
205 | }; | ||
206 | } | ||
207 | const range = { | ||
208 | from: tokenBefore?.from || context.pos, | ||
209 | to: tokenBefore?.to || context.pos, | ||
210 | }; | ||
211 | if (this.shouldReturnCachedCompletion(tokenBefore)) { | ||
212 | log.trace('Returning cached completion result'); | ||
213 | // Postcondition of `shouldReturnCachedCompletion`: `lastCompletion !== null` | ||
214 | return { | ||
215 | ...this.lastCompletion as CompletionResult, | ||
216 | ...range, | ||
217 | }; | ||
218 | } | ||
219 | const entries = await this.fetchContentAssist(context); | ||
220 | if (context.aborted) { | ||
221 | return { | ||
222 | ...range, | ||
223 | options: [], | ||
224 | }; | ||
225 | } | ||
226 | const options: Completion[] = []; | ||
227 | entries.forEach((entry) => { | ||
228 | options.push({ | ||
229 | label: entry.proposal, | ||
230 | detail: entry.description, | ||
231 | info: entry.documentation, | ||
232 | type: entry.kind?.toLowerCase(), | ||
233 | boost: entry.kind === 'KEYWORD' ? -90 : 0, | ||
234 | }); | ||
235 | }); | ||
236 | log.debug('Fetched', options.length, 'completions from server'); | ||
237 | this.lastCompletion = { | ||
238 | ...range, | ||
239 | options, | ||
240 | span: /[a-zA-Z0-9_:]/, | ||
241 | }; | ||
242 | return this.lastCompletion; | ||
243 | } | ||
244 | |||
245 | private shouldReturnCachedCompletion( | ||
246 | token: { from: number, to: number, text: string } | null, | ||
247 | ) { | ||
248 | if (token === null || this.lastCompletion === null) { | ||
249 | return false; | ||
250 | } | ||
251 | const { from, to, text } = token; | ||
252 | const { from: lastFrom, to: lastTo, span } = this.lastCompletion; | ||
253 | if (!lastTo) { | ||
254 | return true; | ||
255 | } | ||
256 | const transformedFrom = this.dirtyChanges.mapPos(lastFrom); | ||
257 | const transformedTo = this.dirtyChanges.mapPos(lastTo, 1); | ||
258 | return from >= transformedFrom && to <= transformedTo && span && span.exec(text); | ||
259 | } | ||
260 | |||
261 | private shouldInvalidateCachedCompletion(transaction: Transaction) { | ||
262 | if (this.lastCompletion === null) { | ||
263 | return false; | ||
264 | } | ||
265 | const { from: lastFrom, to: lastTo } = this.lastCompletion; | ||
266 | if (!lastTo) { | ||
267 | return true; | ||
268 | } | ||
269 | const transformedFrom = this.dirtyChanges.mapPos(lastFrom); | ||
270 | const transformedTo = this.dirtyChanges.mapPos(lastTo, 1); | ||
271 | let invalidate = false; | ||
272 | transaction.changes.iterChangedRanges((fromA, toA) => { | ||
273 | if (fromA < transformedFrom || toA > transformedTo) { | ||
274 | invalidate = true; | ||
275 | } | ||
276 | }); | ||
277 | return invalidate; | ||
278 | } | ||
279 | |||
280 | private async fetchContentAssist(context: CompletionContext) { | ||
281 | await this.prepareForDeltaUpdate(); | ||
282 | const delta = this.computeDelta(); | ||
283 | if (delta === null) { | ||
284 | // Poscondition of `prepareForDeltaUpdate`: `xtextStateId !== null` | ||
285 | return this.doFetchContentAssist(context, this.xtextStateId as string); | ||
286 | } | ||
287 | log.trace('Editor delta', delta); | ||
288 | return await this.withUpdate(async () => { | ||
289 | const result = await this.webSocketClient.send({ | ||
290 | requiredStateId: this.xtextStateId, | ||
291 | ...this.computeContentAssistParams(context), | ||
292 | ...delta, | ||
293 | }); | ||
294 | if (isContentAssistResult(result)) { | ||
295 | return [result.stateId, result.entries]; | ||
296 | } | ||
297 | if (isInvalidStateIdConflictResult(result)) { | ||
298 | const [newStateId] = await this.doFallbackToUpdateFullText(); | ||
299 | if (context.aborted) { | ||
300 | return [newStateId, [] as IContentAssistEntry[]]; | ||
301 | } | ||
302 | const entries = await this.doFetchContentAssist(context, newStateId); | ||
303 | return [newStateId, entries]; | ||
304 | } | ||
305 | log.error('Unextpected content assist result with delta update', result); | ||
306 | throw new Error('Unexpexted content assist result with delta update'); | ||
307 | }); | ||
308 | } | ||
309 | |||
310 | private async doFetchContentAssist(context: CompletionContext, expectedStateId: string) { | ||
311 | const result = await this.webSocketClient.send({ | ||
312 | requiredStateId: expectedStateId, | ||
313 | ...this.computeContentAssistParams(context), | ||
314 | }); | ||
315 | if (isContentAssistResult(result) && result.stateId === expectedStateId) { | ||
316 | return result.entries; | ||
317 | } | ||
318 | log.error('Unexpected content assist result', result); | ||
319 | throw new Error('Unexpected content assist result'); | ||
320 | } | ||
321 | |||
322 | private computeContentAssistParams(context: CompletionContext) { | ||
323 | const tokenBefore = context.tokenBefore(['QualifiedName']); | ||
324 | let selection = {}; | ||
325 | if (tokenBefore !== null) { | ||
326 | selection = { | ||
327 | selectionStart: tokenBefore.from, | ||
328 | selectionEnd: tokenBefore.to, | ||
329 | }; | ||
330 | } | ||
331 | return { | ||
332 | resource: this.resourceName, | ||
333 | serviceType: 'assist', | ||
334 | caretOffset: tokenBefore?.from || context.pos, | ||
335 | ...selection, | ||
336 | }; | ||
337 | } | ||
338 | |||
339 | private computeDelta() { | ||
340 | if (this.dirtyChanges.empty) { | ||
341 | return null; | ||
342 | } | ||
343 | let minFromA = Number.MAX_SAFE_INTEGER; | ||
344 | let maxToA = 0; | ||
345 | let minFromB = Number.MAX_SAFE_INTEGER; | ||
346 | let maxToB = 0; | ||
347 | this.dirtyChanges.iterChangedRanges((fromA, toA, fromB, toB) => { | ||
348 | minFromA = Math.min(minFromA, fromA); | ||
349 | maxToA = Math.max(maxToA, toA); | ||
350 | minFromB = Math.min(minFromB, fromB); | ||
351 | maxToB = Math.max(maxToB, toB); | ||
352 | }); | ||
353 | return { | ||
354 | deltaOffset: minFromA, | ||
355 | deltaReplaceLength: maxToA - minFromA, | ||
356 | deltaText: this.store.state.doc.sliceString(minFromB, maxToB), | ||
357 | }; | ||
358 | } | ||
359 | |||
360 | private async withUpdate<T>(callback: () => Promise<[string, T]>): Promise<T> { | ||
361 | if (this.pendingUpdate !== null) { | ||
362 | throw new Error('Another update is pending, will not perform update'); | ||
363 | } | ||
364 | this.pendingUpdate = this.dirtyChanges; | ||
365 | this.dirtyChanges = this.newEmptyChangeDesc(); | ||
366 | let newStateId: string | null = null; | ||
367 | try { | ||
368 | let result: T; | ||
369 | [newStateId, result] = await callback(); | ||
370 | this.xtextStateId = newStateId; | ||
371 | this.pendingUpdate = null; | ||
372 | // Copy `updateListeners` so that we don't get into a race condition | ||
373 | // if one of the listeners adds another listener. | ||
374 | const listeners = this.updateListeners; | ||
375 | this.updateListeners = []; | ||
376 | listeners.forEach((listener) => { | ||
377 | listener.resolve(); | ||
378 | }); | ||
379 | return result; | ||
380 | } catch (e) { | ||
381 | log.error('Error while update', e); | ||
382 | if (this.pendingUpdate === null) { | ||
383 | log.error('pendingUpdate was cleared during update'); | ||
384 | } else { | ||
385 | this.dirtyChanges = this.pendingUpdate.composeDesc(this.dirtyChanges); | ||
386 | } | ||
387 | this.pendingUpdate = null; | ||
388 | this.webSocketClient.forceReconnectOnError(); | ||
389 | const listeners = this.updateListeners; | ||
390 | this.updateListeners = []; | ||
391 | listeners.forEach((listener) => { | ||
392 | listener.reject(e); | ||
393 | }); | ||
394 | throw e; | ||
395 | } | ||
396 | } | ||
397 | |||
398 | private async prepareForDeltaUpdate() { | ||
399 | if (this.pendingUpdate === null) { | ||
400 | if (this.xtextStateId === null) { | ||
401 | return; | ||
402 | } | ||
403 | await this.updateFullText(); | ||
404 | } | ||
405 | let nowMs = Date.now(); | ||
406 | const endMs = nowMs + WAIT_FOR_UPDATE_TIMEOUT_MS; | ||
407 | while (this.pendingUpdate !== null && nowMs < endMs) { | ||
408 | const timeoutMs = endMs - nowMs; | ||
409 | const promise = new Promise((resolve, reject) => { | ||
410 | const task = new PendingTask(resolve, reject, timeoutMs); | ||
411 | this.updateListeners.push(task); | ||
412 | }); | ||
413 | // We must keep waiting uptil the update has completed, | ||
414 | // so the tasks can't be started in parallel. | ||
415 | // eslint-disable-next-line no-await-in-loop | ||
416 | await promise; | ||
417 | nowMs = Date.now(); | ||
418 | } | ||
419 | if (this.pendingUpdate !== null || this.xtextStateId === null) { | ||
420 | log.error('No successful update in', WAIT_FOR_UPDATE_TIMEOUT_MS, 'ms'); | ||
421 | throw new Error('Failed to wait for successful update'); | ||
422 | } | ||
423 | } | ||
424 | } | ||
diff --git a/language-web/src/main/js/editor/XtextWebSocketClient.ts b/language-web/src/main/js/editor/XtextWebSocketClient.ts deleted file mode 100644 index 5b775500..00000000 --- a/language-web/src/main/js/editor/XtextWebSocketClient.ts +++ /dev/null | |||
@@ -1,345 +0,0 @@ | |||
1 | import { nanoid } from 'nanoid'; | ||
2 | |||
3 | import { getLogger } from '../logging'; | ||
4 | import { PendingTask } from '../utils/PendingTask'; | ||
5 | import { Timer } from '../utils/Timer'; | ||
6 | import { | ||
7 | isErrorResponse, | ||
8 | isOkResponse, | ||
9 | isPushMessage, | ||
10 | IXtextWebRequest, | ||
11 | } from './xtextMessages'; | ||
12 | import { isPongResult } from './xtextServiceResults'; | ||
13 | |||
14 | const XTEXT_SUBPROTOCOL_V1 = 'tools.refinery.language.web.xtext.v1'; | ||
15 | |||
16 | const WEBSOCKET_CLOSE_OK = 1000; | ||
17 | |||
18 | const RECONNECT_DELAY_MS = [200, 1000, 5000, 30_000]; | ||
19 | |||
20 | const MAX_RECONNECT_DELAY_MS = RECONNECT_DELAY_MS[RECONNECT_DELAY_MS.length - 1]; | ||
21 | |||
22 | const BACKGROUND_IDLE_TIMEOUT_MS = 5 * 60 * 1000; | ||
23 | |||
24 | const PING_TIMEOUT_MS = 10 * 1000; | ||
25 | |||
26 | const REQUEST_TIMEOUT_MS = 1000; | ||
27 | |||
28 | const log = getLogger('XtextWebSocketClient'); | ||
29 | |||
30 | type ReconnectHandler = () => Promise<void>; | ||
31 | |||
32 | type PushHandler = ( | ||
33 | resourceId: string, | ||
34 | stateId: string, | ||
35 | service: string, | ||
36 | data: unknown, | ||
37 | ) => Promise<void>; | ||
38 | |||
39 | enum State { | ||
40 | Initial, | ||
41 | Opening, | ||
42 | TabVisible, | ||
43 | TabHiddenIdle, | ||
44 | TabHiddenWaiting, | ||
45 | Error, | ||
46 | TimedOut, | ||
47 | } | ||
48 | |||
49 | export class XtextWebSocketClient { | ||
50 | nextMessageId = 0; | ||
51 | |||
52 | connection!: WebSocket; | ||
53 | |||
54 | pendingRequests = new Map<string, PendingTask<unknown>>(); | ||
55 | |||
56 | onReconnect: ReconnectHandler; | ||
57 | |||
58 | onPush: PushHandler; | ||
59 | |||
60 | state = State.Initial; | ||
61 | |||
62 | reconnectTryCount = 0; | ||
63 | |||
64 | idleTimer = new Timer(() => { | ||
65 | this.handleIdleTimeout(); | ||
66 | }, BACKGROUND_IDLE_TIMEOUT_MS); | ||
67 | |||
68 | pingTimer = new Timer(() => { | ||
69 | this.sendPing(); | ||
70 | }, PING_TIMEOUT_MS); | ||
71 | |||
72 | reconnectTimer = new Timer(() => { | ||
73 | this.handleReconnect(); | ||
74 | }); | ||
75 | |||
76 | constructor(onReconnect: ReconnectHandler, onPush: PushHandler) { | ||
77 | this.onReconnect = onReconnect; | ||
78 | this.onPush = onPush; | ||
79 | document.addEventListener('visibilitychange', () => { | ||
80 | this.handleVisibilityChange(); | ||
81 | }); | ||
82 | this.reconnect(); | ||
83 | } | ||
84 | |||
85 | private get isLogicallyClosed(): boolean { | ||
86 | return this.state === State.Error || this.state === State.TimedOut; | ||
87 | } | ||
88 | |||
89 | get isOpen(): boolean { | ||
90 | return this.state === State.TabVisible | ||
91 | || this.state === State.TabHiddenIdle | ||
92 | || this.state === State.TabHiddenWaiting; | ||
93 | } | ||
94 | |||
95 | private reconnect() { | ||
96 | if (this.isOpen || this.state === State.Opening) { | ||
97 | log.error('Trying to reconnect from', this.state); | ||
98 | return; | ||
99 | } | ||
100 | this.state = State.Opening; | ||
101 | const webSocketServer = window.origin.replace(/^http/, 'ws'); | ||
102 | const webSocketUrl = `${webSocketServer}/xtext-service`; | ||
103 | this.connection = new WebSocket(webSocketUrl, XTEXT_SUBPROTOCOL_V1); | ||
104 | this.connection.addEventListener('open', () => { | ||
105 | if (this.connection.protocol !== XTEXT_SUBPROTOCOL_V1) { | ||
106 | log.error('Unknown subprotocol', this.connection.protocol, 'selected by server'); | ||
107 | this.forceReconnectOnError(); | ||
108 | } | ||
109 | if (document.visibilityState === 'hidden') { | ||
110 | this.handleTabHidden(); | ||
111 | } else { | ||
112 | this.handleTabVisibleConnected(); | ||
113 | } | ||
114 | log.info('Connected to websocket'); | ||
115 | this.nextMessageId = 0; | ||
116 | this.reconnectTryCount = 0; | ||
117 | this.pingTimer.schedule(); | ||
118 | this.onReconnect().catch((error) => { | ||
119 | log.error('Unexpected error in onReconnect handler', error); | ||
120 | }); | ||
121 | }); | ||
122 | this.connection.addEventListener('error', (event) => { | ||
123 | log.error('Unexpected websocket error', event); | ||
124 | this.forceReconnectOnError(); | ||
125 | }); | ||
126 | this.connection.addEventListener('message', (event) => { | ||
127 | this.handleMessage(event.data); | ||
128 | }); | ||
129 | this.connection.addEventListener('close', (event) => { | ||
130 | if (this.isLogicallyClosed && event.code === WEBSOCKET_CLOSE_OK | ||
131 | && this.pendingRequests.size === 0) { | ||
132 | log.info('Websocket closed'); | ||
133 | return; | ||
134 | } | ||
135 | log.error('Websocket closed unexpectedly', event.code, event.reason); | ||
136 | this.forceReconnectOnError(); | ||
137 | }); | ||
138 | } | ||
139 | |||
140 | private handleVisibilityChange() { | ||
141 | if (document.visibilityState === 'hidden') { | ||
142 | if (this.state === State.TabVisible) { | ||
143 | this.handleTabHidden(); | ||
144 | } | ||
145 | return; | ||
146 | } | ||
147 | this.idleTimer.cancel(); | ||
148 | if (this.state === State.TabHiddenIdle || this.state === State.TabHiddenWaiting) { | ||
149 | this.handleTabVisibleConnected(); | ||
150 | return; | ||
151 | } | ||
152 | if (this.state === State.TimedOut) { | ||
153 | this.reconnect(); | ||
154 | } | ||
155 | } | ||
156 | |||
157 | private handleTabHidden() { | ||
158 | log.debug('Tab hidden while websocket is connected'); | ||
159 | this.state = State.TabHiddenIdle; | ||
160 | this.idleTimer.schedule(); | ||
161 | } | ||
162 | |||
163 | private handleTabVisibleConnected() { | ||
164 | log.debug('Tab visible while websocket is connected'); | ||
165 | this.state = State.TabVisible; | ||
166 | } | ||
167 | |||
168 | private handleIdleTimeout() { | ||
169 | log.trace('Waiting for pending tasks before disconnect'); | ||
170 | if (this.state === State.TabHiddenIdle) { | ||
171 | this.state = State.TabHiddenWaiting; | ||
172 | this.handleWaitingForDisconnect(); | ||
173 | } | ||
174 | } | ||
175 | |||
176 | private handleWaitingForDisconnect() { | ||
177 | if (this.state !== State.TabHiddenWaiting) { | ||
178 | return; | ||
179 | } | ||
180 | const pending = this.pendingRequests.size; | ||
181 | if (pending === 0) { | ||
182 | log.info('Closing idle websocket'); | ||
183 | this.state = State.TimedOut; | ||
184 | this.closeConnection(1000, 'idle timeout'); | ||
185 | return; | ||
186 | } | ||
187 | log.info('Waiting for', pending, 'pending requests before closing websocket'); | ||
188 | } | ||
189 | |||
190 | private sendPing() { | ||
191 | if (!this.isOpen) { | ||
192 | return; | ||
193 | } | ||
194 | const ping = nanoid(); | ||
195 | log.trace('Ping', ping); | ||
196 | this.send({ ping }).then((result) => { | ||
197 | if (isPongResult(result) && result.pong === ping) { | ||
198 | log.trace('Pong', ping); | ||
199 | this.pingTimer.schedule(); | ||
200 | } else { | ||
201 | log.error('Invalid pong'); | ||
202 | this.forceReconnectOnError(); | ||
203 | } | ||
204 | }).catch((error) => { | ||
205 | log.error('Error while waiting for ping', error); | ||
206 | this.forceReconnectOnError(); | ||
207 | }); | ||
208 | } | ||
209 | |||
210 | send(request: unknown): Promise<unknown> { | ||
211 | if (!this.isOpen) { | ||
212 | throw new Error('Not open'); | ||
213 | } | ||
214 | const messageId = this.nextMessageId.toString(16); | ||
215 | if (messageId in this.pendingRequests) { | ||
216 | log.error('Message id wraparound still pending', messageId); | ||
217 | this.rejectRequest(messageId, new Error('Message id wraparound')); | ||
218 | } | ||
219 | if (this.nextMessageId >= Number.MAX_SAFE_INTEGER) { | ||
220 | this.nextMessageId = 0; | ||
221 | } else { | ||
222 | this.nextMessageId += 1; | ||
223 | } | ||
224 | const message = JSON.stringify({ | ||
225 | id: messageId, | ||
226 | request, | ||
227 | } as IXtextWebRequest); | ||
228 | log.trace('Sending message', message); | ||
229 | return new Promise((resolve, reject) => { | ||
230 | const task = new PendingTask(resolve, reject, REQUEST_TIMEOUT_MS, () => { | ||
231 | this.removePendingRequest(messageId); | ||
232 | }); | ||
233 | this.pendingRequests.set(messageId, task); | ||
234 | this.connection.send(message); | ||
235 | }); | ||
236 | } | ||
237 | |||
238 | private handleMessage(messageStr: unknown) { | ||
239 | if (typeof messageStr !== 'string') { | ||
240 | log.error('Unexpected binary message', messageStr); | ||
241 | this.forceReconnectOnError(); | ||
242 | return; | ||
243 | } | ||
244 | log.trace('Incoming websocket message', messageStr); | ||
245 | let message: unknown; | ||
246 | try { | ||
247 | message = JSON.parse(messageStr); | ||
248 | } catch (error) { | ||
249 | log.error('Json parse error', error); | ||
250 | this.forceReconnectOnError(); | ||
251 | return; | ||
252 | } | ||
253 | if (isOkResponse(message)) { | ||
254 | this.resolveRequest(message.id, message.response); | ||
255 | } else if (isErrorResponse(message)) { | ||
256 | this.rejectRequest(message.id, new Error(`${message.error} error: ${message.message}`)); | ||
257 | if (message.error === 'server') { | ||
258 | log.error('Reconnecting due to server error: ', message.message); | ||
259 | this.forceReconnectOnError(); | ||
260 | } | ||
261 | } else if (isPushMessage(message)) { | ||
262 | this.onPush( | ||
263 | message.resource, | ||
264 | message.stateId, | ||
265 | message.service, | ||
266 | message.push, | ||
267 | ).catch((error) => { | ||
268 | log.error('Unexpected error in onPush handler', error); | ||
269 | }); | ||
270 | } else { | ||
271 | log.error('Unexpected websocket message', message); | ||
272 | this.forceReconnectOnError(); | ||
273 | } | ||
274 | } | ||
275 | |||
276 | private resolveRequest(messageId: string, value: unknown) { | ||
277 | const pendingRequest = this.pendingRequests.get(messageId); | ||
278 | if (pendingRequest) { | ||
279 | pendingRequest.resolve(value); | ||
280 | this.removePendingRequest(messageId); | ||
281 | return; | ||
282 | } | ||
283 | log.error('Trying to resolve unknown request', messageId, 'with', value); | ||
284 | } | ||
285 | |||
286 | private rejectRequest(messageId: string, reason?: unknown) { | ||
287 | const pendingRequest = this.pendingRequests.get(messageId); | ||
288 | if (pendingRequest) { | ||
289 | pendingRequest.reject(reason); | ||
290 | this.removePendingRequest(messageId); | ||
291 | return; | ||
292 | } | ||
293 | log.error('Trying to reject unknown request', messageId, 'with', reason); | ||
294 | } | ||
295 | |||
296 | private removePendingRequest(messageId: string) { | ||
297 | this.pendingRequests.delete(messageId); | ||
298 | this.handleWaitingForDisconnect(); | ||
299 | } | ||
300 | |||
301 | forceReconnectOnError(): void { | ||
302 | if (this.isLogicallyClosed) { | ||
303 | return; | ||
304 | } | ||
305 | this.abortPendingRequests(); | ||
306 | this.closeConnection(1000, 'reconnecting due to error'); | ||
307 | log.error('Reconnecting after delay due to error'); | ||
308 | this.handleErrorState(); | ||
309 | } | ||
310 | |||
311 | private abortPendingRequests() { | ||
312 | this.pendingRequests.forEach((request) => { | ||
313 | request.reject(new Error('Websocket disconnect')); | ||
314 | }); | ||
315 | this.pendingRequests.clear(); | ||
316 | } | ||
317 | |||
318 | private closeConnection(code: number, reason: string) { | ||
319 | this.pingTimer.cancel(); | ||
320 | const { readyState } = this.connection; | ||
321 | if (readyState !== WebSocket.CLOSING && readyState !== WebSocket.CLOSED) { | ||
322 | this.connection.close(code, reason); | ||
323 | } | ||
324 | } | ||
325 | |||
326 | private handleErrorState() { | ||
327 | this.state = State.Error; | ||
328 | this.reconnectTryCount += 1; | ||
329 | const delay = RECONNECT_DELAY_MS[this.reconnectTryCount - 1] || MAX_RECONNECT_DELAY_MS; | ||
330 | log.info('Reconnecting in', delay, 'ms'); | ||
331 | this.reconnectTimer.schedule(delay); | ||
332 | } | ||
333 | |||
334 | private handleReconnect() { | ||
335 | if (this.state !== State.Error) { | ||
336 | log.error('Unexpected reconnect in', this.state); | ||
337 | return; | ||
338 | } | ||
339 | if (document.visibilityState === 'hidden') { | ||
340 | this.state = State.TimedOut; | ||
341 | } else { | ||
342 | this.reconnect(); | ||
343 | } | ||
344 | } | ||
345 | } | ||
diff --git a/language-web/src/main/js/editor/folding.ts b/language-web/src/main/js/editor/folding.ts deleted file mode 100644 index 54c7294d..00000000 --- a/language-web/src/main/js/editor/folding.ts +++ /dev/null | |||
@@ -1,97 +0,0 @@ | |||
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 deleted file mode 100644 index b2f0134b..00000000 --- a/language-web/src/main/js/editor/indentation.ts +++ /dev/null | |||
@@ -1,84 +0,0 @@ | |||
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 deleted file mode 100644 index cf940698..00000000 --- a/language-web/src/main/js/editor/problem.grammar +++ /dev/null | |||
@@ -1,129 +0,0 @@ | |||
1 | @top Problem { statement* } | ||
2 | |||
3 | statement { | ||
4 | ProblemDeclaration { | ||
5 | ckw<"problem"> QualifiedName "." | ||
6 | } | | ||
7 | ClassDefinition { | ||
8 | ckw<"abstract">? ckw<"class"> RelationName | ||
9 | (ckw<"extends"> sep<",", RelationName>)? | ||
10 | (ClassBody { "{" ReferenceDeclaration* "}" } | ".") | ||
11 | } | | ||
12 | EnumDefinition { | ||
13 | ckw<"enum"> RelationName | ||
14 | (EnumBody { "{" sep<",", UniqueNodeName> "}" } | ".") | ||
15 | } | | ||
16 | PredicateDefinition { | ||
17 | (ckw<"error"> ckw<"pred">? | ckw<"pred">) RelationName ParameterList<Parameter>? | ||
18 | PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." } | ||
19 | } | | ||
20 | Assertion { | ||
21 | ckw<"default">? (NotOp | UnknownOp)? RelationName | ||
22 | ParameterList<AssertionArgument> (":" LogicValue)? "." | ||
23 | } | | ||
24 | NodeValueAssertion { | ||
25 | UniqueNodeName ":" Constant "." | ||
26 | } | | ||
27 | UniqueDeclaration { | ||
28 | ckw<"unique"> sep<",", UniqueNodeName> "." | ||
29 | } | | ||
30 | ScopeDeclaration { | ||
31 | ckw<"scope"> sep<",", ScopeElement> "." | ||
32 | } | ||
33 | } | ||
34 | |||
35 | ReferenceDeclaration { | ||
36 | (kw<"refers"> | kw<"contains">)? | ||
37 | RelationName | ||
38 | RelationName | ||
39 | ( "[" Multiplicity? "]" )? | ||
40 | (kw<"opposite"> RelationName)? | ||
41 | ";"? | ||
42 | } | ||
43 | |||
44 | Parameter { RelationName? VariableName } | ||
45 | |||
46 | Conjunction { ("," | Literal)+ } | ||
47 | |||
48 | OrOp { ";" } | ||
49 | |||
50 | Literal { NotOp? Atom } | ||
51 | |||
52 | Atom { RelationName ParameterList<Argument>? } | ||
53 | |||
54 | Argument { VariableName | Constant } | ||
55 | |||
56 | AssertionArgument { NodeName | StarArgument | Constant } | ||
57 | |||
58 | Constant { Real | String } | ||
59 | |||
60 | LogicValue { | ||
61 | ckw<"true"> | ckw<"false"> | ckw<"unknown"> | ckw<"error"> | ||
62 | } | ||
63 | |||
64 | ScopeElement { RelationName ("=" | "+=") Multiplicity } | ||
65 | |||
66 | Multiplicity { (IntMult "..")? (IntMult | StarMult)} | ||
67 | |||
68 | RelationName { QualifiedName } | ||
69 | |||
70 | UniqueNodeName { QualifiedName } | ||
71 | |||
72 | VariableName { QualifiedName } | ||
73 | |||
74 | NodeName { QualifiedName } | ||
75 | |||
76 | QualifiedName { identifier ("::" identifier)* } | ||
77 | |||
78 | kw<term> { @specialize[@name={term}]<identifier, term> } | ||
79 | |||
80 | ckw<term> { @extend[@name={term}]<identifier, term> } | ||
81 | |||
82 | ParameterList<content> { "(" sep<",", content> ")" } | ||
83 | |||
84 | sep<separator, content> { sep1<separator, content>? } | ||
85 | |||
86 | sep1<separator, content> { content (separator content?)* } | ||
87 | |||
88 | @skip { LineComment | BlockComment | whitespace } | ||
89 | |||
90 | @tokens { | ||
91 | whitespace { std.whitespace+ } | ||
92 | |||
93 | LineComment { ("//" | "%") ![\n]* } | ||
94 | |||
95 | BlockComment { "/*" blockCommentRest } | ||
96 | |||
97 | blockCommentRest { ![*] blockCommentRest | "*" blockCommentAfterStar } | ||
98 | |||
99 | blockCommentAfterStar { "/" | "*" blockCommentAfterStar | ![/*] blockCommentRest } | ||
100 | |||
101 | @precedence { BlockComment, LineComment } | ||
102 | |||
103 | identifier { $[A-Za-z_] $[a-zA-Z0-9_]* } | ||
104 | |||
105 | int { $[0-9]+ } | ||
106 | |||
107 | IntMult { int } | ||
108 | |||
109 | StarMult { "*" } | ||
110 | |||
111 | Real { "-"? (exponential | int ("." (int | exponential))?) } | ||
112 | |||
113 | exponential { int ("e" | "E") ("+" | "-")? int } | ||
114 | |||
115 | String { | ||
116 | "'" (![\\'\n] | "\\" ![\n] | "\\\n")+ "'" | | ||
117 | "\"" (![\\"\n] | "\\" (![\n] | "\n"))* "\"" | ||
118 | } | ||
119 | |||
120 | NotOp { "!" } | ||
121 | |||
122 | UnknownOp { "?" } | ||
123 | |||
124 | StarArgument { "*" } | ||
125 | |||
126 | "{" "}" "(" ")" "[" "]" "." ".." "," ":" "<->" | ||
127 | } | ||
128 | |||
129 | @detectDelim | ||
diff --git a/language-web/src/main/js/editor/problemLanguageSupport.ts b/language-web/src/main/js/editor/problemLanguageSupport.ts deleted file mode 100644 index c9e61b31..00000000 --- a/language-web/src/main/js/editor/problemLanguageSupport.ts +++ /dev/null | |||
@@ -1,83 +0,0 @@ | |||
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 extends 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 | String: t.string, | ||
38 | 'RelationName/QualifiedName': t.typeName, | ||
39 | 'UniqueNodeName/QualifiedName': t.atom, | ||
40 | 'VariableName/QualifiedName': t.variableName, | ||
41 | '{ }': t.brace, | ||
42 | '( )': t.paren, | ||
43 | '[ ]': t.squareBracket, | ||
44 | '. .. , :': t.separator, | ||
45 | '<->': t.definitionOperator, | ||
46 | }), | ||
47 | indentNodeProp.add({ | ||
48 | ProblemDeclaration: indentDeclaration, | ||
49 | UniqueDeclaration: indentDeclaration, | ||
50 | ScopeDeclaration: indentDeclaration, | ||
51 | PredicateBody: indentPredicate, | ||
52 | BlockComment: indentBlockComment, | ||
53 | }), | ||
54 | foldNodeProp.add({ | ||
55 | ClassBody: foldInside, | ||
56 | EnumBody: foldInside, | ||
57 | ParameterList: foldInside, | ||
58 | PredicateBody: foldInside, | ||
59 | Conjunction: foldConjunction, | ||
60 | UniqueDeclaration: foldDeclaration, | ||
61 | ScopeDeclaration: foldDeclaration, | ||
62 | BlockComment: foldBlockComment, | ||
63 | }), | ||
64 | ], | ||
65 | }); | ||
66 | |||
67 | const problemLanguage = LRLanguage.define({ | ||
68 | parser: parserWithMetadata, | ||
69 | languageData: { | ||
70 | commentTokens: { | ||
71 | block: { | ||
72 | open: '/*', | ||
73 | close: '*/', | ||
74 | }, | ||
75 | line: '%', | ||
76 | }, | ||
77 | indentOnInput: /^\s*(?:\{|\}|\(|\)|;|\.)$/, | ||
78 | }, | ||
79 | }); | ||
80 | |||
81 | export function problemLanguageSupport(): LanguageSupport { | ||
82 | return new LanguageSupport(problemLanguage); | ||
83 | } | ||
diff --git a/language-web/src/main/js/editor/xtextMessages.ts b/language-web/src/main/js/editor/xtextMessages.ts deleted file mode 100644 index 68737958..00000000 --- a/language-web/src/main/js/editor/xtextMessages.ts +++ /dev/null | |||
@@ -1,62 +0,0 @@ | |||
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 === 'object' | ||
16 | && typeof okResponse.id === 'string' | ||
17 | && typeof okResponse.response !== 'undefined'; | ||
18 | } | ||
19 | |||
20 | export const VALID_XTEXT_WEB_ERROR_KINDS = ['request', 'server'] as const; | ||
21 | |||
22 | export type XtextWebErrorKind = typeof VALID_XTEXT_WEB_ERROR_KINDS[number]; | ||
23 | |||
24 | export function isXtextWebErrorKind(value: unknown): value is XtextWebErrorKind { | ||
25 | return typeof value === 'string' | ||
26 | && VALID_XTEXT_WEB_ERROR_KINDS.includes(value as XtextWebErrorKind); | ||
27 | } | ||
28 | |||
29 | export interface IXtextWebErrorResponse { | ||
30 | id: string; | ||
31 | |||
32 | error: XtextWebErrorKind; | ||
33 | |||
34 | message: string; | ||
35 | } | ||
36 | |||
37 | export function isErrorResponse(response: unknown): response is IXtextWebErrorResponse { | ||
38 | const errorResponse = response as IXtextWebErrorResponse; | ||
39 | return typeof errorResponse === 'object' | ||
40 | && typeof errorResponse.id === 'string' | ||
41 | && isXtextWebErrorKind(errorResponse.error) | ||
42 | && typeof errorResponse.message === 'string'; | ||
43 | } | ||
44 | |||
45 | export interface IXtextWebPushMessage { | ||
46 | resource: string; | ||
47 | |||
48 | stateId: string; | ||
49 | |||
50 | service: string; | ||
51 | |||
52 | push: unknown; | ||
53 | } | ||
54 | |||
55 | export function isPushMessage(response: unknown): response is IXtextWebPushMessage { | ||
56 | const pushMessage = response as IXtextWebPushMessage; | ||
57 | return typeof pushMessage === 'object' | ||
58 | && typeof pushMessage.resource === 'string' | ||
59 | && typeof pushMessage.stateId === 'string' | ||
60 | && typeof pushMessage.service === 'string' | ||
61 | && typeof pushMessage.push !== 'undefined'; | ||
62 | } | ||
diff --git a/language-web/src/main/js/editor/xtextServiceResults.ts b/language-web/src/main/js/editor/xtextServiceResults.ts deleted file mode 100644 index 6c3d9daf..00000000 --- a/language-web/src/main/js/editor/xtextServiceResults.ts +++ /dev/null | |||
@@ -1,200 +0,0 @@ | |||
1 | export interface IPongResult { | ||
2 | pong: string; | ||
3 | } | ||
4 | |||
5 | export function isPongResult(result: unknown): result is IPongResult { | ||
6 | const pongResult = result as IPongResult; | ||
7 | return typeof pongResult === 'object' | ||
8 | && typeof pongResult.pong === 'string'; | ||
9 | } | ||
10 | |||
11 | export interface IDocumentStateResult { | ||
12 | stateId: string; | ||
13 | } | ||
14 | |||
15 | export function isDocumentStateResult(result: unknown): result is IDocumentStateResult { | ||
16 | const documentStateResult = result as IDocumentStateResult; | ||
17 | return typeof documentStateResult === 'object' | ||
18 | && typeof documentStateResult.stateId === 'string'; | ||
19 | } | ||
20 | |||
21 | export const VALID_CONFLICTS = ['invalidStateId', 'canceled'] as const; | ||
22 | |||
23 | export type Conflict = typeof VALID_CONFLICTS[number]; | ||
24 | |||
25 | export function isConflict(value: unknown): value is Conflict { | ||
26 | return typeof value === 'string' && VALID_CONFLICTS.includes(value as Conflict); | ||
27 | } | ||
28 | |||
29 | export interface IServiceConflictResult { | ||
30 | conflict: Conflict; | ||
31 | } | ||
32 | |||
33 | export function isServiceConflictResult(result: unknown): result is IServiceConflictResult { | ||
34 | const serviceConflictResult = result as IServiceConflictResult; | ||
35 | return typeof serviceConflictResult === 'object' | ||
36 | && isConflict(serviceConflictResult.conflict); | ||
37 | } | ||
38 | |||
39 | export function isInvalidStateIdConflictResult(result: unknown): boolean { | ||
40 | return isServiceConflictResult(result) && result.conflict === 'invalidStateId'; | ||
41 | } | ||
42 | |||
43 | export const VALID_SEVERITIES = ['error', 'warning', 'info', 'ignore'] as const; | ||
44 | |||
45 | export type Severity = typeof VALID_SEVERITIES[number]; | ||
46 | |||
47 | export function isSeverity(value: unknown): value is Severity { | ||
48 | return typeof value === 'string' && VALID_SEVERITIES.includes(value as Severity); | ||
49 | } | ||
50 | |||
51 | export interface IIssue { | ||
52 | description: string; | ||
53 | |||
54 | severity: Severity; | ||
55 | |||
56 | line: number; | ||
57 | |||
58 | column: number; | ||
59 | |||
60 | offset: number; | ||
61 | |||
62 | length: number; | ||
63 | } | ||
64 | |||
65 | export function isIssue(value: unknown): value is IIssue { | ||
66 | const issue = value as IIssue; | ||
67 | return typeof issue === 'object' | ||
68 | && typeof issue.description === 'string' | ||
69 | && isSeverity(issue.severity) | ||
70 | && typeof issue.line === 'number' | ||
71 | && typeof issue.column === 'number' | ||
72 | && typeof issue.offset === 'number' | ||
73 | && typeof issue.length === 'number'; | ||
74 | } | ||
75 | |||
76 | export interface IValidationResult { | ||
77 | issues: IIssue[]; | ||
78 | } | ||
79 | |||
80 | function isArrayOfType<T>(value: unknown, check: (entry: unknown) => entry is T): value is T[] { | ||
81 | return Array.isArray(value) && (value as T[]).every(check); | ||
82 | } | ||
83 | |||
84 | export function isValidationResult(result: unknown): result is IValidationResult { | ||
85 | const validationResult = result as IValidationResult; | ||
86 | return typeof validationResult === 'object' | ||
87 | && isArrayOfType(validationResult.issues, isIssue); | ||
88 | } | ||
89 | |||
90 | export interface IReplaceRegion { | ||
91 | offset: number; | ||
92 | |||
93 | length: number; | ||
94 | |||
95 | text: string; | ||
96 | } | ||
97 | |||
98 | export function isReplaceRegion(value: unknown): value is IReplaceRegion { | ||
99 | const replaceRegion = value as IReplaceRegion; | ||
100 | return typeof replaceRegion === 'object' | ||
101 | && typeof replaceRegion.offset === 'number' | ||
102 | && typeof replaceRegion.length === 'number' | ||
103 | && typeof replaceRegion.text === 'string'; | ||
104 | } | ||
105 | |||
106 | export interface ITextRegion { | ||
107 | offset: number; | ||
108 | |||
109 | length: number; | ||
110 | } | ||
111 | |||
112 | export function isTextRegion(value: unknown): value is ITextRegion { | ||
113 | const textRegion = value as ITextRegion; | ||
114 | return typeof textRegion === 'object' | ||
115 | && typeof textRegion.offset === 'number' | ||
116 | && typeof textRegion.length === 'number'; | ||
117 | } | ||
118 | |||
119 | export const VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS = [ | ||
120 | 'TEXT', | ||
121 | 'METHOD', | ||
122 | 'FUNCTION', | ||
123 | 'CONSTRUCTOR', | ||
124 | 'FIELD', | ||
125 | 'VARIABLE', | ||
126 | 'CLASS', | ||
127 | 'INTERFACE', | ||
128 | 'MODULE', | ||
129 | 'PROPERTY', | ||
130 | 'UNIT', | ||
131 | 'VALUE', | ||
132 | 'ENUM', | ||
133 | 'KEYWORD', | ||
134 | 'SNIPPET', | ||
135 | 'COLOR', | ||
136 | 'FILE', | ||
137 | 'REFERENCE', | ||
138 | 'UNKNOWN', | ||
139 | ] as const; | ||
140 | |||
141 | export type XtextContentAssistEntryKind = typeof VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS[number]; | ||
142 | |||
143 | export function isXtextContentAssistEntryKind( | ||
144 | value: unknown, | ||
145 | ): value is XtextContentAssistEntryKind { | ||
146 | return typeof value === 'string' | ||
147 | && VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS.includes(value as XtextContentAssistEntryKind); | ||
148 | } | ||
149 | |||
150 | export interface IContentAssistEntry { | ||
151 | prefix: string; | ||
152 | |||
153 | proposal: string; | ||
154 | |||
155 | label?: string; | ||
156 | |||
157 | description?: string; | ||
158 | |||
159 | documentation?: string; | ||
160 | |||
161 | escapePosition?: number; | ||
162 | |||
163 | textReplacements: IReplaceRegion[]; | ||
164 | |||
165 | editPositions: ITextRegion[]; | ||
166 | |||
167 | kind: XtextContentAssistEntryKind | string; | ||
168 | } | ||
169 | |||
170 | function isStringOrUndefined(value: unknown): value is string | undefined { | ||
171 | return typeof value === 'string' || typeof value === 'undefined'; | ||
172 | } | ||
173 | |||
174 | function isNumberOrUndefined(value: unknown): value is number | undefined { | ||
175 | return typeof value === 'number' || typeof value === 'undefined'; | ||
176 | } | ||
177 | |||
178 | export function isContentAssistEntry(value: unknown): value is IContentAssistEntry { | ||
179 | const entry = value as IContentAssistEntry; | ||
180 | return typeof entry === 'object' | ||
181 | && typeof entry.prefix === 'string' | ||
182 | && typeof entry.proposal === 'string' | ||
183 | && isStringOrUndefined(entry.label) | ||
184 | && isStringOrUndefined(entry.description) | ||
185 | && isStringOrUndefined(entry.documentation) | ||
186 | && isNumberOrUndefined(entry.escapePosition) | ||
187 | && isArrayOfType(entry.textReplacements, isReplaceRegion) | ||
188 | && isArrayOfType(entry.editPositions, isTextRegion) | ||
189 | && typeof entry.kind === 'string'; | ||
190 | } | ||
191 | |||
192 | export interface IContentAssistResult extends IDocumentStateResult { | ||
193 | entries: IContentAssistEntry[]; | ||
194 | } | ||
195 | |||
196 | export function isContentAssistResult(result: unknown): result is IContentAssistResult { | ||
197 | const contentAssistResult = result as IContentAssistResult; | ||
198 | return isDocumentStateResult(result) | ||
199 | && isArrayOfType(contentAssistResult.entries, isContentAssistEntry); | ||
200 | } | ||