infoview/goals: fix off-by-one error in goal numbering #277
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Reported-by: Hugo Herbelin <[email protected]>
ejgallego
approved these changes
Feb 3, 2023
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Feb 15, 2023
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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Reported-by: Hugo Herbelin [email protected]