Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[documentSymbol] Stream / delay results #124

Closed
ejgallego opened this issue Dec 27, 2022 · 2 comments · Fixed by #141 or ocaml/opam-repository#22956
Closed

[documentSymbol] Stream / delay results #124

ejgallego opened this issue Dec 27, 2022 · 2 comments · Fixed by #141 or ocaml/opam-repository#22956

Comments

@ejgallego
Copy link
Owner

ejgallego commented Dec 27, 2022

Currently textDocument/documentSymbols will only be served when the document checking is complete.

This is far from ideal, so we can either postpone it to a "document completed queue" or even better, stream the results.

Both will require a modification to the request serving architecture.

Implementing the streaming part could actually be used by documentDiagnostics for example (c.f. #49 )

@ejgallego ejgallego added this to the 0.1.2 milestone Dec 27, 2022
ejgallego added a commit that referenced this issue Jan 3, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 3, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 3, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 3, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
@ejgallego ejgallego modified the milestones: 0.1.2, 0.1.3 Jan 4, 2023
@ejgallego
Copy link
Owner Author

When should fleche give back control to the handler so it can process pending requests is a bit of an open question, maybe we'd like to do that in a time-based heuristic? Still unsure, for now let's let the client drive that with the interruption.

@Alizter
Copy link
Collaborator

Alizter commented Jan 5, 2023

@ejgallego I agree with using interruption for the time being. We can experiment with another technique in the future.

ejgallego added a commit that referenced this issue Jan 11, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 11, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 11, 2023
…ocument changes

This should help with #124.

Note that this will make the changes in #136 to use `find_opt` easier.
ejgallego added a commit that referenced this issue Jan 11, 2023
Some requests need to be delayed until the document is ready, such as
`documentSymbols`. In order to do this, we allow to postpone requests,
and `Doc_manager.check` will now return the list of requests pending
for a given document.

The implementation is lightweight and quite a prototype, but should
serve as a basis for more advanced stuff.

Closes #124.
ejgallego added a commit that referenced this issue Jan 11, 2023
Some requests need to be delayed until the document is ready, such as
`documentSymbols`. In order to do this, we allow to postpone requests,
and `Doc_manager.check` will now return the list of requests pending
for a given document.

The implementation is lightweight and quite a prototype, but should
serve as a basis for more advanced stuff.

Closes #124.
ejgallego added a commit that referenced this issue Jan 11, 2023
Some requests need to be delayed until the document is ready, such as
`documentSymbols`. In order to do this, we allow to postpone requests,
and `Doc_manager.check` will now return the list of requests pending
for a given document.

The implementation is lightweight and quite a prototype, but should
serve as a basis for more advanced stuff.

Closes #124.
ejgallego added a commit that referenced this issue Jan 11, 2023
Some requests need to be delayed until the document is ready, such as
`documentSymbols`. In order to do this, we allow to postpone requests,
and `Doc_manager.check` will now return the list of requests pending
for a given document.

The implementation is lightweight and quite a prototype, but should
serve as a basis for more advanced stuff.

Closes #124.
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jan 15, 2023
CHANGES:

----------------------

 - Much improved handling of Coq fatal errors, the server is now
   hardened against them (@ejgallego, ejgallego/coq-lsp#155, ejgallego/coq-lsp#157, ejgallego/coq-lsp#160, fixes ejgallego/coq-lsp#91)
 - `coq-lsp` now follows the LSP specification regarding
   initialization strictly (@ejgallego, ejgallego/coq-lsp#168)
 - New setting for goals to be updated when the selection changes due
   to a command; this makes VsCodeVim cursor tracking work; thanks to
   Cactus (Anton) Golov for detailed bug reporting and testing
   (@ejgallego, @jesyspa, ejgallego/coq-lsp#170, fixes ejgallego/coq-lsp#163)
 - `coq-lsp` will now warn the user when two files have been opened
   simultaneously and the parser may go into a broken state :/
   (@ejgallego, ejgallego/coq-lsp#169)
 - Implement request postponement and cancellation. Thus
   `documentSymbols` will now be postponed until the document is
   ready, (@ejgallego, ejgallego/coq-lsp#141, ejgallego/coq-lsp#146, fixes ejgallego/coq-lsp#124)
 - Protocol and VS Code interfaces now support shelved and given_up
   goals (@ejgallego, ejgallego/coq-lsp#175)
 - Allow to postpone requests to wait for data to become available on
   document points; this is implemented to provide a nicer "show goals
   while I type" experience. Client default has been changed to "show
   goals on mouse, click, typing, and cursor movement) (@ejgallego,
   ejgallego/coq-lsp#177, ejgallego/coq-lsp#179)
 - Store stats per document (@ejgallego, ejgallego/coq-lsp#180, fixes ejgallego/coq-lsp#173)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants