diff options
Diffstat (limited to 'subprojects/frontend/src/xtext/OccurrencesService.ts')
-rw-r--r-- | subprojects/frontend/src/xtext/OccurrencesService.ts | 34 |
1 files changed, 26 insertions, 8 deletions
diff --git a/subprojects/frontend/src/xtext/OccurrencesService.ts b/subprojects/frontend/src/xtext/OccurrencesService.ts index 21fe8644..35913f43 100644 --- a/subprojects/frontend/src/xtext/OccurrencesService.ts +++ b/subprojects/frontend/src/xtext/OccurrencesService.ts | |||
@@ -1,7 +1,10 @@ | |||
1 | import { Transaction } from '@codemirror/state'; | 1 | import { Transaction } from '@codemirror/state'; |
2 | 2 | ||
3 | import type EditorStore from '../editor/EditorStore'; | 3 | import type EditorStore from '../editor/EditorStore'; |
4 | import type { IOccurrence } from '../editor/findOccurrences'; | 4 | import { |
5 | type IOccurrence, | ||
6 | isCursorWithinOccurence, | ||
7 | } from '../editor/findOccurrences'; | ||
5 | import Timer from '../utils/Timer'; | 8 | import Timer from '../utils/Timer'; |
6 | import getLogger from '../utils/getLogger'; | 9 | import getLogger from '../utils/getLogger'; |
7 | 10 | ||
@@ -15,10 +18,6 @@ import { | |||
15 | 18 | ||
16 | const FIND_OCCURRENCES_TIMEOUT_MS = 1000; | 19 | const FIND_OCCURRENCES_TIMEOUT_MS = 1000; |
17 | 20 | ||
18 | // Must clear occurrences asynchronously from `onTransaction`, | ||
19 | // because we must not emit a conflicting transaction when handling the pending transaction. | ||
20 | const CLEAR_OCCURRENCES_TIMEOUT_MS = 10; | ||
21 | |||
22 | const log = getLogger('xtext.OccurrencesService'); | 21 | const log = getLogger('xtext.OccurrencesService'); |
23 | 22 | ||
24 | function transformOccurrences(regions: TextRegion[]): IOccurrence[] { | 23 | function transformOccurrences(regions: TextRegion[]): IOccurrence[] { |
@@ -49,7 +48,7 @@ export default class OccurrencesService { | |||
49 | 48 | ||
50 | private readonly clearOccurrencesTimer = new Timer(() => { | 49 | private readonly clearOccurrencesTimer = new Timer(() => { |
51 | this.clearOccurrences(); | 50 | this.clearOccurrences(); |
52 | }, CLEAR_OCCURRENCES_TIMEOUT_MS); | 51 | }); |
53 | 52 | ||
54 | constructor( | 53 | constructor( |
55 | store: EditorStore, | 54 | store: EditorStore, |
@@ -63,12 +62,27 @@ export default class OccurrencesService { | |||
63 | 62 | ||
64 | onTransaction(transaction: Transaction): void { | 63 | onTransaction(transaction: Transaction): void { |
65 | if (transaction.docChanged) { | 64 | if (transaction.docChanged) { |
65 | // Must clear occurrences asynchronously from `onTransaction`, | ||
66 | // because we must not emit a conflicting transaction when handling the pending transaction. | ||
66 | this.clearOccurrencesTimer.schedule(); | 67 | this.clearOccurrencesTimer.schedule(); |
67 | this.findOccurrencesTimer.reschedule(); | 68 | this.findOccurrencesTimer.reschedule(); |
69 | return; | ||
68 | } | 70 | } |
69 | if (transaction.isUserEvent('select')) { | 71 | if (!transaction.isUserEvent('select')) { |
70 | this.findOccurrencesTimer.reschedule(); | 72 | return; |
71 | } | 73 | } |
74 | if (this.needsOccurrences) { | ||
75 | if (!isCursorWithinOccurence(this.store.state)) { | ||
76 | this.clearOccurrencesTimer.schedule(); | ||
77 | this.findOccurrencesTimer.reschedule(); | ||
78 | } | ||
79 | } else { | ||
80 | this.clearOccurrencesTimer.schedule(); | ||
81 | } | ||
82 | } | ||
83 | |||
84 | private get needsOccurrences(): boolean { | ||
85 | return this.store.state.selection.main.empty; | ||
72 | } | 86 | } |
73 | 87 | ||
74 | private handleFindOccurrences() { | 88 | private handleFindOccurrences() { |
@@ -80,6 +94,10 @@ export default class OccurrencesService { | |||
80 | } | 94 | } |
81 | 95 | ||
82 | private async updateOccurrences() { | 96 | private async updateOccurrences() { |
97 | if (!this.needsOccurrences) { | ||
98 | this.clearOccurrences(); | ||
99 | return; | ||
100 | } | ||
83 | await this.updateService.update(); | 101 | await this.updateService.update(); |
84 | const result = await this.webSocketClient.send({ | 102 | const result = await this.webSocketClient.send({ |
85 | resource: this.updateService.resourceName, | 103 | resource: this.updateService.resourceName, |