coq-lsp
coq-lsp copied to clipboard
Improvement for goal display
I have been running into an issue with the goal display of the vscode client that's a bit annoying. The display for big case analysis does not collapse when entering bullets. A toggle option to eagerly collapse bullets would be great.
Moreover, the page always scroll down to prioritize displaying the goals on bottom instead of the ones on the top. For most use cases, displaying the context would be more helpful.
Additionally, while the default printer with syntax highlighting looks great, it is not very responsive when displaying a long list of goals. The string and layout-engine printers are much faster but don't look as nice.
I am also frequently bitten by this issue and I kept meaning to open an issue about it. Thanks for doing so. I would suggest that we collapse goals by default and make it a configurable behaviour as I think mathcomp routinely work on multiple goals at the same time, so the user should have control over the default behaviour.
I opened a similar issue, but about larger goals https://github.com/ejgallego/coq-lsp/issues/485 and the scrolling behaviour. Additionally, we should have a way to collapse hypotheses too, but I suppose that's another issue.