aboutsummaryrefslogtreecommitdiffstats
path: root/language-web/src/main/js/editor
diff options
context:
space:
mode:
Diffstat (limited to 'language-web/src/main/js/editor')
-rw-r--r--language-web/src/main/js/editor/EditorStore.ts4
-rw-r--r--language-web/src/main/js/editor/XtextClient.ts424
-rw-r--r--language-web/src/main/js/editor/XtextWebSocketClient.ts345
-rw-r--r--language-web/src/main/js/editor/folding.ts97
-rw-r--r--language-web/src/main/js/editor/indentation.ts84
-rw-r--r--language-web/src/main/js/editor/problem.grammar129
-rw-r--r--language-web/src/main/js/editor/problemLanguageSupport.ts83
-rw-r--r--language-web/src/main/js/editor/xtextMessages.ts62
-rw-r--r--language-web/src/main/js/editor/xtextServiceResults.ts200
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
45import { problemLanguageSupport } from '../language/problemLanguageSupport';
45import { getLogger } from '../logging'; 46import { getLogger } from '../logging';
46import { problemLanguageSupport } from './problemLanguageSupport';
47import type { ThemeStore } from '../theme/ThemeStore'; 47import type { ThemeStore } from '../theme/ThemeStore';
48import { XtextClient } from './XtextClient'; 48import { XtextClient } from '../xtext/XtextClient';
49 49
50const log = getLogger('EditorStore'); 50const 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 @@
1import {
2 Completion,
3 CompletionContext,
4 CompletionResult,
5} from '@codemirror/autocomplete';
6import type { Diagnostic } from '@codemirror/lint';
7import {
8 ChangeDesc,
9 ChangeSet,
10 Transaction,
11} from '@codemirror/state';
12import { nanoid } from 'nanoid';
13
14import type { EditorStore } from './EditorStore';
15import { getLogger } from '../logging';
16import { Timer } from '../utils/Timer';
17import {
18 IContentAssistEntry,
19 isContentAssistResult,
20 isDocumentStateResult,
21 isInvalidStateIdConflictResult,
22 isValidationResult,
23} from './xtextServiceResults';
24import { XtextWebSocketClient } from './XtextWebSocketClient';
25import { PendingTask } from '../utils/PendingTask';
26
27const UPDATE_TIMEOUT_MS = 500;
28
29const WAIT_FOR_UPDATE_TIMEOUT_MS = 1000;
30
31const log = getLogger('XtextClient');
32
33export 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 @@
1import { nanoid } from 'nanoid';
2
3import { getLogger } from '../logging';
4import { PendingTask } from '../utils/PendingTask';
5import { Timer } from '../utils/Timer';
6import {
7 isErrorResponse,
8 isOkResponse,
9 isPushMessage,
10 IXtextWebRequest,
11} from './xtextMessages';
12import { isPongResult } from './xtextServiceResults';
13
14const XTEXT_SUBPROTOCOL_V1 = 'tools.refinery.language.web.xtext.v1';
15
16const WEBSOCKET_CLOSE_OK = 1000;
17
18const RECONNECT_DELAY_MS = [200, 1000, 5000, 30_000];
19
20const MAX_RECONNECT_DELAY_MS = RECONNECT_DELAY_MS[RECONNECT_DELAY_MS.length - 1];
21
22const BACKGROUND_IDLE_TIMEOUT_MS = 5 * 60 * 1000;
23
24const PING_TIMEOUT_MS = 10 * 1000;
25
26const REQUEST_TIMEOUT_MS = 1000;
27
28const log = getLogger('XtextWebSocketClient');
29
30type ReconnectHandler = () => Promise<void>;
31
32type PushHandler = (
33 resourceId: string,
34 stateId: string,
35 service: string,
36 data: unknown,
37) => Promise<void>;
38
39enum State {
40 Initial,
41 Opening,
42 TabVisible,
43 TabHiddenIdle,
44 TabHiddenWaiting,
45 Error,
46 TimedOut,
47}
48
49export 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 @@
1import { EditorState } from '@codemirror/state';
2import type { SyntaxNode } from '@lezer/common';
3
4export 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 */
12export 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 */
50export 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 */
78export 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 @@
1import { 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 */
13function 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 */
61function 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
69export function indentBlockComment(): number {
70 // Do not indent.
71 return -1;
72}
73
74export function indentDeclaration(context: TreeIndentContext): number {
75 return indentDeclarationStrategy(context, 1);
76}
77
78export 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
3statement {
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
35ReferenceDeclaration {
36 (kw<"refers"> | kw<"contains">)?
37 RelationName
38 RelationName
39 ( "[" Multiplicity? "]" )?
40 (kw<"opposite"> RelationName)?
41 ";"?
42}
43
44Parameter { RelationName? VariableName }
45
46Conjunction { ("," | Literal)+ }
47
48OrOp { ";" }
49
50Literal { NotOp? Atom }
51
52Atom { RelationName ParameterList<Argument>? }
53
54Argument { VariableName | Constant }
55
56AssertionArgument { NodeName | StarArgument | Constant }
57
58Constant { Real | String }
59
60LogicValue {
61 ckw<"true"> | ckw<"false"> | ckw<"unknown"> | ckw<"error">
62}
63
64ScopeElement { RelationName ("=" | "+=") Multiplicity }
65
66Multiplicity { (IntMult "..")? (IntMult | StarMult)}
67
68RelationName { QualifiedName }
69
70UniqueNodeName { QualifiedName }
71
72VariableName { QualifiedName }
73
74NodeName { QualifiedName }
75
76QualifiedName { identifier ("::" identifier)* }
77
78kw<term> { @specialize[@name={term}]<identifier, term> }
79
80ckw<term> { @extend[@name={term}]<identifier, term> }
81
82ParameterList<content> { "(" sep<",", content> ")" }
83
84sep<separator, content> { sep1<separator, content>? }
85
86sep1<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 @@
1import { styleTags, tags as t } from '@codemirror/highlight';
2import {
3 foldInside,
4 foldNodeProp,
5 indentNodeProp,
6 LanguageSupport,
7 LRLanguage,
8} from '@codemirror/language';
9import { LRParser } from '@lezer/lr';
10
11import { parser } from '../../../../build/generated/sources/lezer/problem';
12import {
13 foldBlockComment,
14 foldConjunction,
15 foldDeclaration,
16} from './folding';
17import {
18 indentBlockComment,
19 indentDeclaration,
20 indentPredicate,
21} from './indentation';
22
23const 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
67const 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
81export 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 @@
1export interface IXtextWebRequest {
2 id: string;
3
4 request: unknown;
5}
6
7export interface IXtextWebOkResponse {
8 id: string;
9
10 response: unknown;
11}
12
13export 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
20export const VALID_XTEXT_WEB_ERROR_KINDS = ['request', 'server'] as const;
21
22export type XtextWebErrorKind = typeof VALID_XTEXT_WEB_ERROR_KINDS[number];
23
24export function isXtextWebErrorKind(value: unknown): value is XtextWebErrorKind {
25 return typeof value === 'string'
26 && VALID_XTEXT_WEB_ERROR_KINDS.includes(value as XtextWebErrorKind);
27}
28
29export interface IXtextWebErrorResponse {
30 id: string;
31
32 error: XtextWebErrorKind;
33
34 message: string;
35}
36
37export 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
45export interface IXtextWebPushMessage {
46 resource: string;
47
48 stateId: string;
49
50 service: string;
51
52 push: unknown;
53}
54
55export 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 @@
1export interface IPongResult {
2 pong: string;
3}
4
5export 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
11export interface IDocumentStateResult {
12 stateId: string;
13}
14
15export 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
21export const VALID_CONFLICTS = ['invalidStateId', 'canceled'] as const;
22
23export type Conflict = typeof VALID_CONFLICTS[number];
24
25export function isConflict(value: unknown): value is Conflict {
26 return typeof value === 'string' && VALID_CONFLICTS.includes(value as Conflict);
27}
28
29export interface IServiceConflictResult {
30 conflict: Conflict;
31}
32
33export function isServiceConflictResult(result: unknown): result is IServiceConflictResult {
34 const serviceConflictResult = result as IServiceConflictResult;
35 return typeof serviceConflictResult === 'object'
36 && isConflict(serviceConflictResult.conflict);
37}
38
39export function isInvalidStateIdConflictResult(result: unknown): boolean {
40 return isServiceConflictResult(result) && result.conflict === 'invalidStateId';
41}
42
43export const VALID_SEVERITIES = ['error', 'warning', 'info', 'ignore'] as const;
44
45export type Severity = typeof VALID_SEVERITIES[number];
46
47export function isSeverity(value: unknown): value is Severity {
48 return typeof value === 'string' && VALID_SEVERITIES.includes(value as Severity);
49}
50
51export 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
65export 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
76export interface IValidationResult {
77 issues: IIssue[];
78}
79
80function 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
84export 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
90export interface IReplaceRegion {
91 offset: number;
92
93 length: number;
94
95 text: string;
96}
97
98export 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
106export interface ITextRegion {
107 offset: number;
108
109 length: number;
110}
111
112export 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
119export 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
141export type XtextContentAssistEntryKind = typeof VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS[number];
142
143export 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
150export 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
170function isStringOrUndefined(value: unknown): value is string | undefined {
171 return typeof value === 'string' || typeof value === 'undefined';
172}
173
174function isNumberOrUndefined(value: unknown): value is number | undefined {
175 return typeof value === 'number' || typeof value === 'undefined';
176}
177
178export 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
192export interface IContentAssistResult extends IDocumentStateResult {
193 entries: IContentAssistEntry[];
194}
195
196export function isContentAssistResult(result: unknown): result is IContentAssistResult {
197 const contentAssistResult = result as IContentAssistResult;
198 return isDocumentStateResult(result)
199 && isArrayOfType(contentAssistResult.entries, isContentAssistEntry);
200}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-09-02 13:33:02 +0000