Display warnings in error browser #195
Comments
|
Indeed I was thinking about this when I introduced the error browser, I'm a bit unsure tho about the HCI story here. For errors, you clearly want to have a dedicated display as it requires action; however, what's the story for warnings? Should these just be addressed by a code action instead? |
|
@ejgallego I was thinking about this again and I noticed something that I didn't make clear before. We don't want the warnings to display all the time, only when we have the cursor over them just like with errors. Having the warnings also display in the error browser (even under a dedicated warnings tab that you can ignore) would be ideal. |
|
At the moment the only way to view the warnings is to hover your mouse over them, and it makes it difficult to read sometimes. |
|
I see what you mean, still not sure about the UI design for this, warnings are already displayed in the diagnostics window, and a code action should happen for the warning (ignore / fix) There is a key difference between warnings and errors: Errors contain complex content, like unification failures, etc... However, warnings are often a single text line, so what is the advantage about having a decidated display over the already standard display? It seems to me that the current display in the list works fine, but I see your point about the workflow with the panel. |
|
I think this could be a good topic to discuss in the next meeting, is it OK if we use the tag to mark such topics? |
|
Having a goal panel, a proof script and a diagnostic panel open is not feasible for people with tiny laptops. |
|
Actually could the diagnostic window maybe docked in a different way? I think we can come with the good UI panel for warnings, but these being actionable, IMHO we need to chat a bit about the design, happy to take a PR tho with a preliminary design. The current error browser has some problems actually too. |
|
I was thinking something like a "warnings browser" under the error browser which can be closed by default. I usually dock my problems to the RHS, by default it is docked to the bottom. I don't finder either particularly appealing when I have two buffers open. |
|
The thing is that if you see a warning, you wanna go to hover and click "fix" right away, don't you? We could duplicate this in the info panel, but certainly low prio IMHO. |
|
I think that #308 plus this is enough as to try something sooner. |
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)
We should display warnings in the error browser, or at least make a new tab for them.
The text was updated successfully, but these errors were encountered: