coq-lsp icon indicating copy to clipboard operation
coq-lsp copied to clipboard

Improvement for goal display

Open qcfu-bu opened this issue 1 year ago • 2 comments

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.

Screenshot 2024-02-26 at 9 46 01 AM

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.

Screenshot 2024-02-26 at 9 42 41 AM

qcfu-bu avatar Feb 26 '24 14:02 qcfu-bu

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.

qcfu-bu avatar Feb 26 '24 16:02 qcfu-bu

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.

Alizter avatar Feb 27 '24 00:02 Alizter