diff options
Diffstat (limited to 'language-web/src/main/js/xtext/XtextClient.ts')
-rw-r--r-- | language-web/src/main/js/xtext/XtextClient.ts | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/language-web/src/main/js/xtext/XtextClient.ts b/language-web/src/main/js/xtext/XtextClient.ts index 03b81b1c..28f3d0cc 100644 --- a/language-web/src/main/js/xtext/XtextClient.ts +++ b/language-web/src/main/js/xtext/XtextClient.ts | |||
@@ -16,21 +16,21 @@ import { XtextWebSocketClient } from './XtextWebSocketClient'; | |||
16 | const log = getLogger('xtext.XtextClient'); | 16 | const log = getLogger('xtext.XtextClient'); |
17 | 17 | ||
18 | export class XtextClient { | 18 | export class XtextClient { |
19 | private webSocketClient: XtextWebSocketClient; | 19 | private readonly webSocketClient: XtextWebSocketClient; |
20 | 20 | ||
21 | private updateService: UpdateService; | 21 | private readonly updateService: UpdateService; |
22 | 22 | ||
23 | private contentAssistService: ContentAssistService; | 23 | private readonly contentAssistService: ContentAssistService; |
24 | 24 | ||
25 | private highlightingService: HighlightingService; | 25 | private readonly highlightingService: HighlightingService; |
26 | 26 | ||
27 | private validationService: ValidationService; | 27 | private readonly validationService: ValidationService; |
28 | 28 | ||
29 | private occurrencesService: OccurrencesService; | 29 | private readonly occurrencesService: OccurrencesService; |
30 | 30 | ||
31 | constructor(store: EditorStore) { | 31 | constructor(store: EditorStore) { |
32 | this.webSocketClient = new XtextWebSocketClient( | 32 | this.webSocketClient = new XtextWebSocketClient( |
33 | () => this.updateService.onConnect(), | 33 | () => this.updateService.onReconnect(), |
34 | (resource, stateId, service, push) => this.onPush(resource, stateId, service, push), | 34 | (resource, stateId, service, push) => this.onPush(resource, stateId, service, push), |
35 | ); | 35 | ); |
36 | this.updateService = new UpdateService(store, this.webSocketClient); | 36 | this.updateService = new UpdateService(store, this.webSocketClient); |
@@ -52,15 +52,17 @@ export class XtextClient { | |||
52 | this.occurrencesService.onTransaction(transaction); | 52 | this.occurrencesService.onTransaction(transaction); |
53 | } | 53 | } |
54 | 54 | ||
55 | private async onPush(resource: string, stateId: string, service: string, push: unknown) { | 55 | private onPush(resource: string, stateId: string, service: string, push: unknown) { |
56 | const { resourceName, xtextStateId } = this.updateService; | 56 | const { resourceName, xtextStateId } = this.updateService; |
57 | if (resource !== resourceName) { | 57 | if (resource !== resourceName) { |
58 | log.error('Unknown resource name: expected:', resourceName, 'got:', resource); | 58 | log.error('Unknown resource name: expected:', resourceName, 'got:', resource); |
59 | return; | 59 | return; |
60 | } | 60 | } |
61 | if (stateId !== xtextStateId) { | 61 | if (stateId !== xtextStateId) { |
62 | log.error('Unexpected xtext state id: expected:', xtextStateId, 'got:', resource); | 62 | log.error('Unexpected xtext state id: expected:', xtextStateId, 'got:', stateId); |
63 | await this.updateService.updateFullText(); | 63 | // The current push message might be stale (referring to a previous state), |
64 | // so this is not neccessarily an error and there is no need to force-reconnect. | ||
65 | return; | ||
64 | } | 66 | } |
65 | switch (service) { | 67 | switch (service) { |
66 | case 'highlight': | 68 | case 'highlight': |