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.

Sign up for GitHub

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

Jump to bottom

Incremental documentSymbol #316

Closed
ejgallego opened this issue Feb 14, 2023 · 0 comments · Fixed by #337 or ocaml/opam-repository#23319
Closed

Incremental documentSymbol #316

ejgallego opened this issue Feb 14, 2023 · 0 comments · Fixed by #337 or ocaml/opam-repository#23319
Labels
kind: enhancement New feature or request kind: internal part: lsp server part: protocol (LSP)
Milestone
0.1.5

Comments

@ejgallego
Copy link
Owner

This will allow us to perform more expensive computations, like types.
@ejgallego ejgallego added this to the 0.1.5 milestone Feb 14, 2023
ejgallego added a commit that referenced this issue Feb 14, 2023
@ejgallego
[info] Improve documentSymbol request to return extended info.
653afa2 
Fixes #121, #122, #316

We improved `documentSymbol` return type for the newer `DocumentSymbol[]`
hierarchical symbol support in recent LSP versions.

Sections and modules will now be properly represented, as well as
constructors for inductive types, projections for records,
etc...
@ejgallego ejgallego mentioned this issue Feb 15, 2023
Merged
@ejgallego ejgallego mentioned this issue Feb 15, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 15, 2023
@ejgallego
[new release] coq-lsp (0.1.5+8.16)
b7a2330 
CHANGES:

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

 - Fix a bug when trying to complete in an empty file (@ejgallego,
   ejgallego/coq-lsp#270)
 - Fix a bug with the position reported by the `$/coq/fileProgress`
   notification
 - Fix messages panel rendering after the port to React (@ejgallego,
   ejgallego/coq-lsp#272)
 - Fix non-compliance with LSP range type due to extra `offset` field
   (@ejgallego, ejgallego/coq-lsp#271)
 - The goal display now numbers goals starting with 1 instead of 0
   (@artagnon, ejgallego/coq-lsp#277, report by Hugo Herbelin)
 - Markdown Coq code blocks now must specify "coq" as a language
   (@ejgallego, ejgallego/coq-lsp#280)
 - Server is now more strict w.r.t. what URIs it will accept for
   documents, see protocol documentation (@ejgallego, ejgallego/coq-lsp#286, reported
   by Alex Sanchez-Stern)
 - Hypotheses with bodies are now correctly displayed (@ejgallego,
   ejgallego/coq-lsp#296, fixes ejgallego/coq-lsp#293, report by Ali Caglayan)
 - `coq-lsp` incorrectly required the optional `rootPath`
   initialization parameter, moreover it ignored `rootUri` if present
   which goes against the LSP spec (@ejgallego, ejgallego/coq-lsp#295, report by Alex
   Sanchez-Stern)
 - `coq-lsp` will now reject opening multiple files when the
   underlying Coq version is buggy (@ejgallego, fixes ejgallego/coq-lsp#275, fixes
   ejgallego/coq-lsp#281)
 - Fix bug when parsing client option for unicode completion
   (@ejgallego ejgallego/coq-lsp#301)
 - Support unicode characters in filenames (@artagnon, ejgallego/coq-lsp#302)
 - Stop checking documents after a maximum number of errors,
   user-configurable (by default 150) (@ejgallego, ejgallego/coq-lsp#303)
 - Coq Markdown files (.mv extension) are now highlighted properly
   using both Coq and Markdown syntax rules (@4ever2, ejgallego/coq-lsp#307)
 - Goal view now supports find (@Alizter, ejgallego/coq-lsp#309, closes ejgallego/coq-lsp#305)
 - coq-lsp now understands a basic version of Coq Waterproof files
   (.wpn) Note that we don't associate to them by default, as to allow
   the waterproof extension to take over the files (@ejgallego, ejgallego/coq-lsp#306)
 - URI validation is now more strict, and some further bugs should be
   solved; note still this can be an issue on some client settings
   (@ejgallego, ejgallego/coq-lsp#313, fixes ejgallego/coq-lsp#187)
 - Display Coq info and debug messages in info panel (@ejgallego,
   ejgallego/coq-lsp#314, fixes ejgallego/coq-lsp#308)
 - Goal display handles background goals better, showing preview,
   goals stack, and focusing information (@ejgallego, ejgallego/coq-lsp#290, fixes
   ejgallego/coq-lsp#288, fixes ejgallego/coq-lsp#304, based on jsCoq code by Shachar Itzhaky)
 - Warnings are now printed in the info view messages panel
   (@ejgallego, ejgallego/coq-lsp#315, fixes ejgallego/coq-lsp#195)
 - Info protocol messages now have location and level
   (@ejgallego, ejgallego/coq-lsp#315)
 - Warnings are not printed in the info view messages panel
   (@ejgallego, #, fixes ejgallego/coq-lsp#195)
 - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
   hierarchical symbol support. This means that sections and modules
   will now be properly represented, as well as constructors for
   inductive types, projections for records, etc...  (@ejgallego,
   ejgallego/coq-lsp#174, fixes ejgallego/coq-lsp#121, ejgallego/coq-lsp#122)
 - [internal] Error recovery can now execute full Coq commands as to
   amend states, required for ejgallego/coq-lsp#319 (@ejallego, ejgallego/coq-lsp#320)
 - Auto-admit the previous bullet goal when a new bullet cannot be
   opened due to an unsolved previous bullet. This also works for {}
   focusing operators. This is very useful when navigating bulleted
   proofs (@ejgallego, @Alizter, ejgallego/coq-lsp#319, fixes ejgallego/coq-lsp#300)
 - Store Ast.Info.t incrementally (@ejgallego, ejgallego/coq-lsp#337, fixes ejgallego/coq-lsp#316)
 - Basic jump to definition support; due to lack of workspace
   metadata, this only works inside the same file (@ejgallego, ejgallego/coq-lsp#318)
 - Show type of identifiers at point on hover (@ejgallego, ejgallego/coq-lsp#321, cc:
   ejgallego/coq-lsp#164)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement New feature or request kind: internal part: lsp server part: protocol (LSP)
Projects
None yet
Milestone
0.1.5
1 participant
@ejgallego