Codemirror deferrers (#3006)

* Force document update requests when necessary

* fix up codemirror deferrers

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* lock

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* fixups kcl/index

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* fix copilot

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* updates

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* updates

Signed-off-by: Jess Frazelle <github@jessfraz.com>

* docs

Signed-off-by: Jess Frazelle <github@jessfraz.com>

---------

Signed-off-by: Jess Frazelle <github@jessfraz.com>
Co-authored-by: Marijn Haverbeke <marijn@haverbeke.berlin>
This commit is contained in:
Jess Frazelle
2024-07-11 16:05:19 -07:00
committed by GitHub
parent 2dd1f0f213
commit 88d9cdc52b
13 changed files with 176 additions and 124 deletions

View File

@ -195,14 +195,15 @@ export class CompletionRequester implements PluginValue {
private queuedUids: string[] = []
private _deffererCodeUpdate = deferExecution(() => {
this.requestCompletions()
}, changesDelay)
private _deffererUserSelect = deferExecution(() => {
this.rejectSuggestionCommand()
}, changesDelay)
// When a doc update needs to be sent to the server, this holds the
// timeout handle for it. When null, the server has the up-to-date
// document.
private sendScheduledInput: number | null = null
constructor(readonly view: EditorView, client: LanguageServerClient) {
this.client = client
}
@ -245,7 +246,34 @@ export class CompletionRequester implements PluginValue {
}
this.lastPos = this.view.state.selection.main.head
if (viewUpdate.docChanged) this._deffererCodeUpdate(true)
if (viewUpdate.docChanged) this.scheduleUpdateDoc()
}
scheduleUpdateDoc() {
if (this.sendScheduledInput != null)
window.clearTimeout(this.sendScheduledInput)
this.sendScheduledInput = window.setTimeout(
() => this.updateDoc(),
changesDelay
)
}
updateDoc() {
if (this.sendScheduledInput != null) {
window.clearTimeout(this.sendScheduledInput)
this.sendScheduledInput = null
}
if (!this.client.ready) return
try {
this.requestCompletions()
} catch (e) {
console.error(e)
}
}
ensureDocUpdated() {
if (this.sendScheduledInput != null) this.updateDoc()
}
ghostText(): GhostText | null {