diff options
Diffstat (limited to 'language-web/src/main/js/xtext/XtextClient.ts')
-rw-r--r-- | language-web/src/main/js/xtext/XtextClient.ts | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/language-web/src/main/js/xtext/XtextClient.ts b/language-web/src/main/js/xtext/XtextClient.ts index 28f3d0cc..3922b230 100644 --- a/language-web/src/main/js/xtext/XtextClient.ts +++ b/language-web/src/main/js/xtext/XtextClient.ts | |||
@@ -12,6 +12,7 @@ import { UpdateService } from './UpdateService'; | |||
12 | import { getLogger } from '../utils/logger'; | 12 | import { getLogger } from '../utils/logger'; |
13 | import { ValidationService } from './ValidationService'; | 13 | import { ValidationService } from './ValidationService'; |
14 | import { XtextWebSocketClient } from './XtextWebSocketClient'; | 14 | import { XtextWebSocketClient } from './XtextWebSocketClient'; |
15 | import { XtextWebPushService } from './xtextMessages'; | ||
15 | 16 | ||
16 | const log = getLogger('xtext.XtextClient'); | 17 | const log = getLogger('xtext.XtextClient'); |
17 | 18 | ||
@@ -52,7 +53,7 @@ export class XtextClient { | |||
52 | this.occurrencesService.onTransaction(transaction); | 53 | this.occurrencesService.onTransaction(transaction); |
53 | } | 54 | } |
54 | 55 | ||
55 | private onPush(resource: string, stateId: string, service: string, push: unknown) { | 56 | private onPush(resource: string, stateId: string, service: XtextWebPushService, push: unknown) { |
56 | const { resourceName, xtextStateId } = this.updateService; | 57 | const { resourceName, xtextStateId } = this.updateService; |
57 | if (resource !== resourceName) { | 58 | if (resource !== resourceName) { |
58 | log.error('Unknown resource name: expected:', resourceName, 'got:', resource); | 59 | log.error('Unknown resource name: expected:', resourceName, 'got:', resource); |
@@ -70,10 +71,6 @@ export class XtextClient { | |||
70 | return; | 71 | return; |
71 | case 'validate': | 72 | case 'validate': |
72 | this.validationService.onPush(push); | 73 | this.validationService.onPush(push); |
73 | return; | ||
74 | default: | ||
75 | log.error('Unknown push service:', service); | ||
76 | break; | ||
77 | } | 74 | } |
78 | } | 75 | } |
79 | 76 | ||