diff options
Diffstat (limited to 'subprojects/frontend/src/xtext/UpdateService.ts')
-rw-r--r-- | subprojects/frontend/src/xtext/UpdateService.ts | 193 |
1 files changed, 116 insertions, 77 deletions
diff --git a/subprojects/frontend/src/xtext/UpdateService.ts b/subprojects/frontend/src/xtext/UpdateService.ts index 2994b11b..f8b71160 100644 --- a/subprojects/frontend/src/xtext/UpdateService.ts +++ b/subprojects/frontend/src/xtext/UpdateService.ts | |||
@@ -27,24 +27,47 @@ const WAIT_FOR_UPDATE_TIMEOUT_MS = 1000; | |||
27 | 27 | ||
28 | const log = getLogger('xtext.UpdateService'); | 28 | const log = getLogger('xtext.UpdateService'); |
29 | 29 | ||
30 | /** | ||
31 | * State effect used to override the dirty changes after a transaction. | ||
32 | * | ||
33 | * If this state effect is _not_ present in a transaction, | ||
34 | * the transaction will be appended to the current dirty changes. | ||
35 | * | ||
36 | * If this state effect is present, the current dirty changes will be replaced | ||
37 | * by the value of this effect. | ||
38 | */ | ||
30 | const setDirtyChanges = StateEffect.define<ChangeSet>(); | 39 | const setDirtyChanges = StateEffect.define<ChangeSet>(); |
31 | 40 | ||
32 | export interface IAbortSignal { | 41 | export interface IAbortSignal { |
33 | aborted: boolean; | 42 | aborted: boolean; |
34 | } | 43 | } |
35 | 44 | ||
45 | interface StateUpdateResult<T> { | ||
46 | newStateId: string; | ||
47 | |||
48 | data: T; | ||
49 | } | ||
50 | |||
51 | interface Delta { | ||
52 | deltaOffset: number; | ||
53 | |||
54 | deltaReplaceLength: number; | ||
55 | |||
56 | deltaText: string; | ||
57 | } | ||
58 | |||
36 | export default class UpdateService { | 59 | export default class UpdateService { |
37 | resourceName: string; | 60 | resourceName: string; |
38 | 61 | ||
39 | xtextStateId: string | null = null; | 62 | xtextStateId: string | undefined; |
40 | 63 | ||
41 | private readonly store: EditorStore; | 64 | private readonly store: EditorStore; |
42 | 65 | ||
43 | /** | 66 | /** |
44 | * The changes being synchronized to the server if a full or delta text update is running, | 67 | * The changes being synchronized to the server if a full or delta text update is running, |
45 | * `null` otherwise. | 68 | * `undefined` otherwise. |
46 | */ | 69 | */ |
47 | private pendingUpdate: ChangeSet | null = null; | 70 | private pendingUpdate: ChangeSet | undefined; |
48 | 71 | ||
49 | /** | 72 | /** |
50 | * Local changes not yet sychronized to the server and not part of the running update, if any. | 73 | * Local changes not yet sychronized to the server and not part of the running update, if any. |
@@ -54,7 +77,7 @@ export default class UpdateService { | |||
54 | private readonly webSocketClient: XtextWebSocketClient; | 77 | private readonly webSocketClient: XtextWebSocketClient; |
55 | 78 | ||
56 | private readonly updatedCondition = new ConditionVariable( | 79 | private readonly updatedCondition = new ConditionVariable( |
57 | () => this.pendingUpdate === null && this.xtextStateId !== null, | 80 | () => this.pendingUpdate === undefined && this.xtextStateId !== undefined, |
58 | WAIT_FOR_UPDATE_TIMEOUT_MS, | 81 | WAIT_FOR_UPDATE_TIMEOUT_MS, |
59 | ); | 82 | ); |
60 | 83 | ||
@@ -70,7 +93,7 @@ export default class UpdateService { | |||
70 | } | 93 | } |
71 | 94 | ||
72 | onReconnect(): void { | 95 | onReconnect(): void { |
73 | this.xtextStateId = null; | 96 | this.xtextStateId = undefined; |
74 | this.updateFullText().catch((error) => { | 97 | this.updateFullText().catch((error) => { |
75 | log.error('Unexpected error during initial update', error); | 98 | log.error('Unexpected error during initial update', error); |
76 | }); | 99 | }); |
@@ -82,7 +105,7 @@ export default class UpdateService { | |||
82 | ) as StateEffect<ChangeSet> | undefined; | 105 | ) as StateEffect<ChangeSet> | undefined; |
83 | if (setDirtyChangesEffect) { | 106 | if (setDirtyChangesEffect) { |
84 | const { value } = setDirtyChangesEffect; | 107 | const { value } = setDirtyChangesEffect; |
85 | if (this.pendingUpdate !== null) { | 108 | if (this.pendingUpdate !== undefined) { |
86 | this.pendingUpdate = ChangeSet.empty(value.length); | 109 | this.pendingUpdate = ChangeSet.empty(value.length); |
87 | } | 110 | } |
88 | this.dirtyChanges = value; | 111 | this.dirtyChanges = value; |
@@ -100,20 +123,20 @@ export default class UpdateService { | |||
100 | * The result reflects any changes that happened since the `xtextStateId` | 123 | * The result reflects any changes that happened since the `xtextStateId` |
101 | * version was uploaded to the server. | 124 | * version was uploaded to the server. |
102 | * | 125 | * |
103 | * @return the summary of changes since the last update | 126 | * @returns the summary of changes since the last update |
104 | */ | 127 | */ |
105 | computeChangesSinceLastUpdate(): ChangeDesc { | 128 | computeChangesSinceLastUpdate(): ChangeDesc { |
106 | return ( | 129 | return ( |
107 | this.pendingUpdate?.composeDesc(this.dirtyChanges.desc) || | 130 | this.pendingUpdate?.composeDesc(this.dirtyChanges.desc) ?? |
108 | this.dirtyChanges.desc | 131 | this.dirtyChanges.desc |
109 | ); | 132 | ); |
110 | } | 133 | } |
111 | 134 | ||
112 | private handleIdleUpdate() { | 135 | private handleIdleUpdate(): void { |
113 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { | 136 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { |
114 | return; | 137 | return; |
115 | } | 138 | } |
116 | if (this.pendingUpdate === null) { | 139 | if (this.pendingUpdate === undefined) { |
117 | this.update().catch((error) => { | 140 | this.update().catch((error) => { |
118 | log.error('Unexpected error during scheduled update', error); | 141 | log.error('Unexpected error during scheduled update', error); |
119 | }); | 142 | }); |
@@ -121,7 +144,7 @@ export default class UpdateService { | |||
121 | this.idleUpdateTimer.reschedule(); | 144 | this.idleUpdateTimer.reschedule(); |
122 | } | 145 | } |
123 | 146 | ||
124 | private newEmptyChangeSet() { | 147 | private newEmptyChangeSet(): ChangeSet { |
125 | return ChangeSet.of([], this.store.state.doc.length); | 148 | return ChangeSet.of([], this.store.state.doc.length); |
126 | } | 149 | } |
127 | 150 | ||
@@ -129,14 +152,14 @@ export default class UpdateService { | |||
129 | await this.withUpdate(() => this.doUpdateFullText()); | 152 | await this.withUpdate(() => this.doUpdateFullText()); |
130 | } | 153 | } |
131 | 154 | ||
132 | private async doUpdateFullText(): Promise<[string, void]> { | 155 | private async doUpdateFullText(): Promise<StateUpdateResult<void>> { |
133 | const result = await this.webSocketClient.send({ | 156 | const result = await this.webSocketClient.send({ |
134 | resource: this.resourceName, | 157 | resource: this.resourceName, |
135 | serviceType: 'update', | 158 | serviceType: 'update', |
136 | fullText: this.store.state.doc.sliceString(0), | 159 | fullText: this.store.state.doc.sliceString(0), |
137 | }); | 160 | }); |
138 | const { stateId } = DocumentStateResult.parse(result); | 161 | const { stateId } = DocumentStateResult.parse(result); |
139 | return [stateId, undefined]; | 162 | return { newStateId: stateId, data: undefined }; |
140 | } | 163 | } |
141 | 164 | ||
142 | /** | 165 | /** |
@@ -146,12 +169,12 @@ export default class UpdateService { | |||
146 | * Performs either an update with delta text or a full text update if needed. | 169 | * Performs either an update with delta text or a full text update if needed. |
147 | * If there are not local dirty changes, the promise resolves immediately. | 170 | * If there are not local dirty changes, the promise resolves immediately. |
148 | * | 171 | * |
149 | * @return a promise resolving when the update is completed | 172 | * @returns a promise resolving when the update is completed |
150 | */ | 173 | */ |
151 | async update(): Promise<void> { | 174 | async update(): Promise<void> { |
152 | await this.prepareForDeltaUpdate(); | 175 | await this.prepareForDeltaUpdate(); |
153 | const delta = this.computeDelta(); | 176 | const delta = this.computeDelta(); |
154 | if (delta === null) { | 177 | if (delta === undefined) { |
155 | return; | 178 | return; |
156 | } | 179 | } |
157 | log.trace('Editor delta', delta); | 180 | log.trace('Editor delta', delta); |
@@ -164,7 +187,10 @@ export default class UpdateService { | |||
164 | }); | 187 | }); |
165 | const parsedDocumentStateResult = DocumentStateResult.safeParse(result); | 188 | const parsedDocumentStateResult = DocumentStateResult.safeParse(result); |
166 | if (parsedDocumentStateResult.success) { | 189 | if (parsedDocumentStateResult.success) { |
167 | return [parsedDocumentStateResult.data.stateId, undefined]; | 190 | return { |
191 | newStateId: parsedDocumentStateResult.data.stateId, | ||
192 | data: undefined, | ||
193 | }; | ||
168 | } | 194 | } |
169 | if (isConflictResult(result, 'invalidStateId')) { | 195 | if (isConflictResult(result, 'invalidStateId')) { |
170 | return this.doFallbackToUpdateFullText(); | 196 | return this.doFallbackToUpdateFullText(); |
@@ -173,12 +199,12 @@ export default class UpdateService { | |||
173 | }); | 199 | }); |
174 | } | 200 | } |
175 | 201 | ||
176 | private doFallbackToUpdateFullText() { | 202 | private doFallbackToUpdateFullText(): Promise<StateUpdateResult<void>> { |
177 | if (this.pendingUpdate === null) { | 203 | if (this.pendingUpdate === undefined) { |
178 | throw new Error('Only a pending update can be extended'); | 204 | throw new Error('Only a pending update can be extended'); |
179 | } | 205 | } |
180 | log.warn('Delta update failed, performing full text update'); | 206 | log.warn('Delta update failed, performing full text update'); |
181 | this.xtextStateId = null; | 207 | this.xtextStateId = undefined; |
182 | this.pendingUpdate = this.pendingUpdate.compose(this.dirtyChanges); | 208 | this.pendingUpdate = this.pendingUpdate.compose(this.dirtyChanges); |
183 | this.dirtyChanges = this.newEmptyChangeSet(); | 209 | this.dirtyChanges = this.newEmptyChangeSet(); |
184 | return this.doUpdateFullText(); | 210 | return this.doUpdateFullText(); |
@@ -193,56 +219,69 @@ export default class UpdateService { | |||
193 | return []; | 219 | return []; |
194 | } | 220 | } |
195 | const delta = this.computeDelta(); | 221 | const delta = this.computeDelta(); |
196 | if (delta !== null) { | 222 | if (delta !== undefined) { |
197 | log.trace('Editor delta', delta); | 223 | log.trace('Editor delta', delta); |
198 | const entries = await this.withUpdate(async () => { | 224 | // Try to fetch while also performing a delta update. |
199 | const result = await this.webSocketClient.send({ | 225 | const fetchUpdateEntries = await this.withUpdate(() => |
200 | ...params, | 226 | this.doFetchContentAssistWithDelta(params, delta), |
201 | requiredStateId: this.xtextStateId, | 227 | ); |
202 | ...delta, | 228 | if (fetchUpdateEntries !== undefined) { |
203 | }); | 229 | return fetchUpdateEntries; |
204 | const parsedContentAssistResult = ContentAssistResult.safeParse(result); | ||
205 | if (parsedContentAssistResult.success) { | ||
206 | const { stateId, entries: resultEntries } = | ||
207 | parsedContentAssistResult.data; | ||
208 | return [stateId, resultEntries]; | ||
209 | } | ||
210 | if (isConflictResult(result, 'invalidStateId')) { | ||
211 | log.warn('Server state invalid during content assist'); | ||
212 | const [newStateId] = await this.doFallbackToUpdateFullText(); | ||
213 | // We must finish this state update transaction to prepare for any push events | ||
214 | // before querying for content assist, so we just return `null` and will query | ||
215 | // the content assist service later. | ||
216 | return [newStateId, null]; | ||
217 | } | ||
218 | throw parsedContentAssistResult.error; | ||
219 | }); | ||
220 | if (entries !== null) { | ||
221 | return entries; | ||
222 | } | 230 | } |
223 | if (signal.aborted) { | 231 | if (signal.aborted) { |
224 | return []; | 232 | return []; |
225 | } | 233 | } |
226 | } | 234 | } |
227 | // Poscondition of `prepareForDeltaUpdate`: `xtextStateId !== null` | 235 | if (this.xtextStateId === undefined) { |
228 | return this.doFetchContentAssist(params, this.xtextStateId as string); | 236 | throw new Error('failed to obtain Xtext state id'); |
237 | } | ||
238 | return this.doFetchContentAssistFetchOnly(params, this.xtextStateId); | ||
229 | } | 239 | } |
230 | 240 | ||
231 | private async doFetchContentAssist( | 241 | private async doFetchContentAssistWithDelta( |
232 | params: Record<string, unknown>, | 242 | params: Record<string, unknown>, |
233 | expectedStateId: string, | 243 | delta: Delta, |
234 | ) { | 244 | ): Promise<StateUpdateResult<ContentAssistEntry[] | undefined>> { |
235 | const result = await this.webSocketClient.send({ | 245 | const fetchUpdateResult = await this.webSocketClient.send({ |
246 | ...params, | ||
247 | requiredStateId: this.xtextStateId, | ||
248 | ...delta, | ||
249 | }); | ||
250 | const parsedContentAssistResult = | ||
251 | ContentAssistResult.safeParse(fetchUpdateResult); | ||
252 | if (parsedContentAssistResult.success) { | ||
253 | const { stateId, entries: resultEntries } = | ||
254 | parsedContentAssistResult.data; | ||
255 | return { newStateId: stateId, data: resultEntries }; | ||
256 | } | ||
257 | if (isConflictResult(fetchUpdateResult, 'invalidStateId')) { | ||
258 | log.warn('Server state invalid during content assist'); | ||
259 | const { newStateId } = await this.doFallbackToUpdateFullText(); | ||
260 | // We must finish this state update transaction to prepare for any push events | ||
261 | // before querying for content assist, so we just return `undefined` and will query | ||
262 | // the content assist service later. | ||
263 | return { newStateId, data: undefined }; | ||
264 | } | ||
265 | throw parsedContentAssistResult.error; | ||
266 | } | ||
267 | |||
268 | private async doFetchContentAssistFetchOnly( | ||
269 | params: Record<string, unknown>, | ||
270 | requiredStateId: string, | ||
271 | ): Promise<ContentAssistEntry[]> { | ||
272 | // Fallback to fetching without a delta update. | ||
273 | const fetchOnlyResult = await this.webSocketClient.send({ | ||
236 | ...params, | 274 | ...params, |
237 | requiredStateId: expectedStateId, | 275 | requiredStateId: this.xtextStateId, |
238 | }); | 276 | }); |
239 | const { stateId, entries } = ContentAssistResult.parse(result); | 277 | const { stateId, entries: fetchOnlyEntries } = |
240 | if (stateId !== expectedStateId) { | 278 | ContentAssistResult.parse(fetchOnlyResult); |
279 | if (stateId !== requiredStateId) { | ||
241 | throw new Error( | 280 | throw new Error( |
242 | `Unexpected state id, expected: ${expectedStateId} got: ${stateId}`, | 281 | `Unexpected state id, expected: ${requiredStateId} got: ${stateId}`, |
243 | ); | 282 | ); |
244 | } | 283 | } |
245 | return entries; | 284 | return fetchOnlyEntries; |
246 | } | 285 | } |
247 | 286 | ||
248 | async formatText(): Promise<void> { | 287 | async formatText(): Promise<void> { |
@@ -253,7 +292,7 @@ export default class UpdateService { | |||
253 | to = this.store.state.doc.length; | 292 | to = this.store.state.doc.length; |
254 | } | 293 | } |
255 | log.debug('Formatting from', from, 'to', to); | 294 | log.debug('Formatting from', from, 'to', to); |
256 | await this.withUpdate(async () => { | 295 | await this.withUpdate<void>(async () => { |
257 | const result = await this.webSocketClient.send({ | 296 | const result = await this.webSocketClient.send({ |
258 | resource: this.resourceName, | 297 | resource: this.resourceName, |
259 | serviceType: 'format', | 298 | serviceType: 'format', |
@@ -266,13 +305,13 @@ export default class UpdateService { | |||
266 | to, | 305 | to, |
267 | insert: formattedText, | 306 | insert: formattedText, |
268 | }); | 307 | }); |
269 | return [stateId, null]; | 308 | return { newStateId: stateId, data: undefined }; |
270 | }); | 309 | }); |
271 | } | 310 | } |
272 | 311 | ||
273 | private computeDelta() { | 312 | private computeDelta(): Delta | undefined { |
274 | if (this.dirtyChanges.empty) { | 313 | if (this.dirtyChanges.empty) { |
275 | return null; | 314 | return undefined; |
276 | } | 315 | } |
277 | let minFromA = Number.MAX_SAFE_INTEGER; | 316 | let minFromA = Number.MAX_SAFE_INTEGER; |
278 | let maxToA = 0; | 317 | let maxToA = 0; |
@@ -291,15 +330,17 @@ export default class UpdateService { | |||
291 | }; | 330 | }; |
292 | } | 331 | } |
293 | 332 | ||
294 | private applyBeforeDirtyChanges(changeSpec: ChangeSpec) { | 333 | private applyBeforeDirtyChanges(changeSpec: ChangeSpec): void { |
295 | const pendingChanges = | 334 | const pendingChanges = |
296 | this.pendingUpdate?.compose(this.dirtyChanges) || this.dirtyChanges; | 335 | this.pendingUpdate?.compose(this.dirtyChanges) ?? this.dirtyChanges; |
297 | const revertChanges = pendingChanges.invert(this.store.state.doc); | 336 | const revertChanges = pendingChanges.invert(this.store.state.doc); |
298 | const applyBefore = ChangeSet.of(changeSpec, revertChanges.newLength); | 337 | const applyBefore = ChangeSet.of(changeSpec, revertChanges.newLength); |
299 | const redoChanges = pendingChanges.map(applyBefore.desc); | 338 | const redoChanges = pendingChanges.map(applyBefore.desc); |
300 | const changeSet = revertChanges.compose(applyBefore).compose(redoChanges); | 339 | const changeSet = revertChanges.compose(applyBefore).compose(redoChanges); |
301 | this.store.dispatch({ | 340 | this.store.dispatch({ |
302 | changes: changeSet, | 341 | changes: changeSet, |
342 | // Keep the current set of dirty changes (but update them according the re-formatting) | ||
343 | // and to not add the formatting the dirty changes. | ||
303 | effects: [setDirtyChanges.of(redoChanges)], | 344 | effects: [setDirtyChanges.of(redoChanges)], |
304 | }); | 345 | }); |
305 | } | 346 | } |
@@ -318,37 +359,35 @@ export default class UpdateService { | |||
318 | * to ensure that the local `stateId` is updated likewise to be able to handle | 359 | * to ensure that the local `stateId` is updated likewise to be able to handle |
319 | * push messages referring to the new `stateId` from the server. | 360 | * push messages referring to the new `stateId` from the server. |
320 | * If additional work is needed to compute the second value in some cases, | 361 | * If additional work is needed to compute the second value in some cases, |
321 | * use `T | null` instead of `T` as a return type and signal the need for additional | 362 | * use `T | undefined` instead of `T` as a return type and signal the need for additional |
322 | * computations by returning `null`. Thus additional computations can be performed | 363 | * computations by returning `undefined`. Thus additional computations can be performed |
323 | * outside of the critical section. | 364 | * outside of the critical section. |
324 | * | 365 | * |
325 | * @param callback the asynchronous callback that updates the server state | 366 | * @param callback the asynchronous callback that updates the server state |
326 | * @return a promise resolving to the second value returned by `callback` | 367 | * @returns a promise resolving to the second value returned by `callback` |
327 | */ | 368 | */ |
328 | private async withUpdate<T>( | 369 | private async withUpdate<T>( |
329 | callback: () => Promise<[string, T]>, | 370 | callback: () => Promise<StateUpdateResult<T>>, |
330 | ): Promise<T> { | 371 | ): Promise<T> { |
331 | if (this.pendingUpdate !== null) { | 372 | if (this.pendingUpdate !== undefined) { |
332 | throw new Error('Another update is pending, will not perform update'); | 373 | throw new Error('Another update is pending, will not perform update'); |
333 | } | 374 | } |
334 | this.pendingUpdate = this.dirtyChanges; | 375 | this.pendingUpdate = this.dirtyChanges; |
335 | this.dirtyChanges = this.newEmptyChangeSet(); | 376 | this.dirtyChanges = this.newEmptyChangeSet(); |
336 | let newStateId: string | null = null; | ||
337 | try { | 377 | try { |
338 | let result: T; | 378 | const { newStateId, data } = await callback(); |
339 | [newStateId, result] = await callback(); | ||
340 | this.xtextStateId = newStateId; | 379 | this.xtextStateId = newStateId; |
341 | this.pendingUpdate = null; | 380 | this.pendingUpdate = undefined; |
342 | this.updatedCondition.notifyAll(); | 381 | this.updatedCondition.notifyAll(); |
343 | return result; | 382 | return data; |
344 | } catch (e) { | 383 | } catch (e) { |
345 | log.error('Error while update', e); | 384 | log.error('Error while update', e); |
346 | if (this.pendingUpdate === null) { | 385 | if (this.pendingUpdate === undefined) { |
347 | log.error('pendingUpdate was cleared during update'); | 386 | log.error('pendingUpdate was cleared during update'); |
348 | } else { | 387 | } else { |
349 | this.dirtyChanges = this.pendingUpdate.compose(this.dirtyChanges); | 388 | this.dirtyChanges = this.pendingUpdate.compose(this.dirtyChanges); |
350 | } | 389 | } |
351 | this.pendingUpdate = null; | 390 | this.pendingUpdate = undefined; |
352 | this.webSocketClient.forceReconnectOnError(); | 391 | this.webSocketClient.forceReconnectOnError(); |
353 | this.updatedCondition.rejectAll(e); | 392 | this.updatedCondition.rejectAll(e); |
354 | throw e; | 393 | throw e; |
@@ -357,16 +396,16 @@ export default class UpdateService { | |||
357 | 396 | ||
358 | /** | 397 | /** |
359 | * Ensures that there is some state available on the server (`xtextStateId`) | 398 | * Ensures that there is some state available on the server (`xtextStateId`) |
360 | * and that there is not pending update. | 399 | * and that there is no pending update. |
361 | * | 400 | * |
362 | * After this function resolves, a delta text update is possible. | 401 | * After this function resolves, a delta text update is possible. |
363 | * | 402 | * |
364 | * @return a promise resolving when there is a valid state id but no pending update | 403 | * @returns a promise resolving when there is a valid state id but no pending update |
365 | */ | 404 | */ |
366 | private async prepareForDeltaUpdate() { | 405 | private async prepareForDeltaUpdate(): Promise<void> { |
367 | // If no update is pending, but the full text hasn't been uploaded to the server yet, | 406 | // If no update is pending, but the full text hasn't been uploaded to the server yet, |
368 | // we must start a full text upload. | 407 | // we must start a full text upload. |
369 | if (this.pendingUpdate === null && this.xtextStateId === null) { | 408 | if (this.pendingUpdate === undefined && this.xtextStateId === undefined) { |
370 | await this.updateFullText(); | 409 | await this.updateFullText(); |
371 | } | 410 | } |
372 | await this.updatedCondition.waitFor(); | 411 | await this.updatedCondition.waitFor(); |