-
Notifications
You must be signed in to change notification settings - Fork 873
Description
Problem
I am working on developing a language server for the rocq prover, https://github.com/coq/vscoq.
I have recently run into a problem with the document outline (in vscode).
In a recent change, I parse the document incrementally, using events that get popped up in an event loop. Many times the textDocument/documentSymbol
request gets sent before the parsing of the document is finished.
Tried solutions
The first solution I explored was using progress based. Unfortunately it seems that vscode does not send a partialResultToken
or a workDoneToken
in the request although I did opt-in through the capabilities. Maybe there is a subtlety I do not understand ?
The second solution I explored comes from the disccusion in #1367 where it is suggested that after receiving a ServerCancelled
error code the client well then re-send the request later. This does not seem to be happening for the documentSymbol
request.
After some digging in the spec, it seems documentSymbol
is not cancellable ? Compared to the semanticTokensClientCapabilities it does not contain the serverCancelledSupport field
.
Proposed solution
Could we add serverCancelled
support to the documentSymbol
request ?
Related
Also related to microsoft/vscode#135453