[doc] [completion] Improve UTF-8 and position validation #270
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
We are now more strict, and require the [Utf8] clients to take an action when the conversion fails. Usually clients doing the conversion for the range will want to select the total length (last character) whereas the clients trying to grab a character will want to abort whatever they are doing. I have reviewed all such uses, and found a couple of errors. This also fixes the bug with the `fileProgress` range due to the above. Re Fixes #264
|
No exception anymore, but we are silently failing to serve the completion request because of the issue in #264, but I guess it doesn't cause any issues when pressing Ctrl + Enter. Interestingly, if you type |
|
So I don't know if we should say it fixes #264, but rather makes it fail cleanly. |
|
Thanks for the testing Ali, I'm glad to hear this works better. Better typing will indeed help in the future.
Yeah, I was thinking about the same. On the other hand, if the client does something inconsistent like in this case, what can we do on our side? I don't see any better way TBH. I'd be happy to keep #264 open if there is some todo in the For now, I'd reopen the upstream bug but in the vscode repos. |
|
I'll then merge this for now, happy to have #264 reopened if we find a way to improve the server. I'll add this problem to the known issues list in the README (at some point to be moved to a different place, but I'd like that list to be very visible for now) |
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.
We are now more strict, and require the [Utf8] clients to take an action when the conversion fails.
Usually clients doing the conversion for the range will want to select the total length (last character) whereas the clients trying to grab a character will want to abort whatever they are doing.
I have reviewed all such uses, and found a couple of errors.
This also fixes the bug with the
fileProgressrange due to the above.Re Fixes #264