Support find in the goal window #305
Labels
Milestone
Comments
|
Yes, actually a first step would be to make lists filtrable like in Lean; search like that may be a bit challenging as we don't have any code context, and the UI toolkit (https://github.com/microsoft/vscode-webview-ui-toolkit) is kinda bare. |
|
Doesn't VS Code already have a search function? Do you know if it is possible to use? |
|
The info view panel is a barebones webview, so all this have to be built from scratch. |
|
@ejgallego Not true, see my PR: #309 |
Oh, indeed, well spotted! |
|
I think that other stuff such as the cursor is not possible without view-side code tho. |
ejgallego
added
kind: enhancement
ejgallego
added a commit
to Alizter/coq-lsp
that referenced
this issue
Feb 9, 2023
Fixes ejgallego#305 Signed-off-by: Ali Caglayan <alizter@gmail.com> <!-- ps-id: e3066447-b19a-48c6-8222-3e15636591c8 -->
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
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
We should support find (Ctrl + f) in the goal window. When you have a large goal, you sometimes might want to search through it.
Current workaround is copy paste the error message in a new buffer.
The text was updated successfully, but these errors were encountered: