diff options
author | 2022-09-05 01:29:11 +0200 | |
---|---|---|
committer | 2022-09-06 01:05:24 +0200 | |
commit | eb94326bb64552dbd7df62ae201ccca37f368467 (patch) | |
tree | b810f0230ace058cac8a6343455ca60113925221 /subprojects/frontend/src/xtext/OccurrencesService.ts | |
parent | refactor(frontend): more readable indentation (diff) | |
download | refinery-eb94326bb64552dbd7df62ae201ccca37f368467.tar.gz refinery-eb94326bb64552dbd7df62ae201ccca37f368467.tar.zst refinery-eb94326bb64552dbd7df62ae201ccca37f368467.zip |
feat(frontend): show connection status
Diffstat (limited to 'subprojects/frontend/src/xtext/OccurrencesService.ts')
-rw-r--r-- | subprojects/frontend/src/xtext/OccurrencesService.ts | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/subprojects/frontend/src/xtext/OccurrencesService.ts b/subprojects/frontend/src/xtext/OccurrencesService.ts index c8d6fd7b..9d738d76 100644 --- a/subprojects/frontend/src/xtext/OccurrencesService.ts +++ b/subprojects/frontend/src/xtext/OccurrencesService.ts | |||
@@ -41,6 +41,15 @@ export default class OccurrencesService { | |||
41 | private readonly updateService: UpdateService, | 41 | private readonly updateService: UpdateService, |
42 | ) {} | 42 | ) {} |
43 | 43 | ||
44 | onReconnect(): void { | ||
45 | this.clearOccurrences(); | ||
46 | this.findOccurrencesLater(); | ||
47 | } | ||
48 | |||
49 | onDisconnect(): void { | ||
50 | this.clearOccurrences(); | ||
51 | } | ||
52 | |||
44 | onTransaction(transaction: Transaction): void { | 53 | onTransaction(transaction: Transaction): void { |
45 | if (transaction.docChanged) { | 54 | if (transaction.docChanged) { |
46 | // Must clear occurrences asynchronously from `onTransaction`, | 55 | // Must clear occurrences asynchronously from `onTransaction`, |
@@ -91,7 +100,7 @@ export default class OccurrencesService { | |||
91 | } | 100 | } |
92 | 101 | ||
93 | private async updateOccurrences() { | 102 | private async updateOccurrences() { |
94 | if (!this.needsOccurrences) { | 103 | if (!this.needsOccurrences || !this.updateService.opened) { |
95 | this.clearOccurrences(); | 104 | this.clearOccurrences(); |
96 | return; | 105 | return; |
97 | } | 106 | } |