diff options
Diffstat (limited to 'language-web/src/main/js/editor/XtextClient.ts')
-rw-r--r-- | language-web/src/main/js/editor/XtextClient.ts | 48 |
1 files changed, 20 insertions, 28 deletions
diff --git a/language-web/src/main/js/editor/XtextClient.ts b/language-web/src/main/js/editor/XtextClient.ts index 1c6c0ae6..5216154e 100644 --- a/language-web/src/main/js/editor/XtextClient.ts +++ b/language-web/src/main/js/editor/XtextClient.ts | |||
@@ -8,6 +8,7 @@ import { nanoid } from 'nanoid'; | |||
8 | 8 | ||
9 | import type { EditorStore } from './EditorStore'; | 9 | import type { EditorStore } from './EditorStore'; |
10 | import { getLogger } from '../logging'; | 10 | import { getLogger } from '../logging'; |
11 | import { Timer } from '../utils/Timer'; | ||
11 | import { | 12 | import { |
12 | isDocumentStateResult, | 13 | isDocumentStateResult, |
13 | isServiceConflictResult, | 14 | isServiceConflictResult, |
@@ -36,7 +37,9 @@ export class XtextClient { | |||
36 | 37 | ||
37 | dirtyChanges: ChangeDesc; | 38 | dirtyChanges: ChangeDesc; |
38 | 39 | ||
39 | updateTimeout: NodeJS.Timeout | null = null; | 40 | updateTimer = new Timer(() => { |
41 | this.handleUpdate(); | ||
42 | }, UPDATE_TIMEOUT_MS); | ||
40 | 43 | ||
41 | store: EditorStore; | 44 | store: EditorStore; |
42 | 45 | ||
@@ -46,15 +49,11 @@ export class XtextClient { | |||
46 | this.store = store; | 49 | this.store = store; |
47 | this.dirtyChanges = this.newEmptyChangeDesc(); | 50 | this.dirtyChanges = this.newEmptyChangeDesc(); |
48 | this.webSocketClient = new XtextWebSocketClient( | 51 | this.webSocketClient = new XtextWebSocketClient( |
49 | () => { | 52 | async () => { |
50 | this.updateFullText().catch((error) => { | 53 | await this.updateFullText(); |
51 | log.error('Unexpected error during initial update', error); | ||
52 | }); | ||
53 | }, | 54 | }, |
54 | (resource, stateId, service, push) => { | 55 | async (resource, stateId, service, push) => { |
55 | this.onPush(resource, stateId, service, push).catch((error) => { | 56 | await this.onPush(resource, stateId, service, push); |
56 | log.error('Unexected error during push message handling', error); | ||
57 | }); | ||
58 | }, | 57 | }, |
59 | ); | 58 | ); |
60 | } | 59 | } |
@@ -62,9 +61,8 @@ export class XtextClient { | |||
62 | onTransaction(transaction: Transaction): void { | 61 | onTransaction(transaction: Transaction): void { |
63 | const { changes } = transaction; | 62 | const { changes } = transaction; |
64 | if (!changes.empty) { | 63 | if (!changes.empty) { |
65 | this.webSocketClient.ensureOpen(); | ||
66 | this.dirtyChanges = this.dirtyChanges.composeDesc(changes.desc); | 64 | this.dirtyChanges = this.dirtyChanges.composeDesc(changes.desc); |
67 | this.scheduleUpdate(); | 65 | this.updateTimer.reschedule(); |
68 | } | 66 | } |
69 | } | 67 | } |
70 | 68 | ||
@@ -118,22 +116,16 @@ export class XtextClient { | |||
118 | return this.pendingUpdate.composeDesc(this.dirtyChanges); | 116 | return this.pendingUpdate.composeDesc(this.dirtyChanges); |
119 | } | 117 | } |
120 | 118 | ||
121 | private scheduleUpdate() { | 119 | private handleUpdate() { |
122 | if (this.updateTimeout !== null) { | 120 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { |
123 | clearTimeout(this.updateTimeout); | 121 | return; |
124 | } | 122 | } |
125 | this.updateTimeout = setTimeout(() => { | 123 | if (!this.pendingUpdate) { |
126 | this.updateTimeout = null; | 124 | this.updateDeltaText().catch((error) => { |
127 | if (!this.webSocketClient.isOpen || this.dirtyChanges.empty) { | 125 | log.error('Unexpected error during scheduled update', error); |
128 | return; | 126 | }); |
129 | } | 127 | } |
130 | if (!this.pendingUpdate) { | 128 | this.updateTimer.reschedule(); |
131 | this.updateDeltaText().catch((error) => { | ||
132 | log.error('Unexpected error during scheduled update', error); | ||
133 | }); | ||
134 | } | ||
135 | this.scheduleUpdate(); | ||
136 | }, UPDATE_TIMEOUT_MS); | ||
137 | } | 129 | } |
138 | 130 | ||
139 | private newEmptyChangeDesc() { | 131 | private newEmptyChangeDesc() { |
@@ -169,7 +161,7 @@ export class XtextClient { | |||
169 | return; | 161 | return; |
170 | } | 162 | } |
171 | const delta = this.computeDelta(); | 163 | const delta = this.computeDelta(); |
172 | log.debug('Editor delta', delta); | 164 | log.trace('Editor delta', delta); |
173 | await this.withUpdate(async () => { | 165 | await this.withUpdate(async () => { |
174 | const result = await this.webSocketClient.send({ | 166 | const result = await this.webSocketClient.send({ |
175 | resource: this.resourceName, | 167 | resource: this.resourceName, |
@@ -231,7 +223,7 @@ export class XtextClient { | |||
231 | this.pendingUpdate = null; | 223 | this.pendingUpdate = null; |
232 | switch (newStateId) { | 224 | switch (newStateId) { |
233 | case UpdateAction.ForceReconnect: | 225 | case UpdateAction.ForceReconnect: |
234 | this.webSocketClient.forceReconnectDueToError(); | 226 | this.webSocketClient.handleApplicationError(); |
235 | break; | 227 | break; |
236 | case UpdateAction.FullTextUpdate: | 228 | case UpdateAction.FullTextUpdate: |
237 | await this.updateFullText(); | 229 | await this.updateFullText(); |