Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for folding ranges #799

Open
rtetley opened this issue Jun 26, 2024 · 3 comments
Open

Add support for folding ranges #799

rtetley opened this issue Jun 26, 2024 · 3 comments
Labels
enhancement New feature or request prio:high

Comments

@rtetley
Copy link
Collaborator

rtetley commented Jun 26, 2024

Fix the folding ranges by letting the server send the ranges contained in Proof. [...] Qed. Or Proof. [...] Admit..
See: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_foldingRange

@rtetley
Copy link
Collaborator Author

rtetley commented Jun 26, 2024

Related to #797, it will use the same mechanism

@Durbatuluk1701
Copy link
Contributor

Can we include a concrete example on what this folding range should look like? I personally feel like the current (2.2.3) folding for Proof bodies is good but maybe am missing a corner case

@rtetley
Copy link
Collaborator Author

rtetley commented Jan 27, 2025

I believe currently this is only handled by vscode through indentation. If you don't add indentation to your proof blocks it won't work (see #137). Also this could add support for folding modules and sections.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request prio:high
Projects
None yet
Development

No branches or pull requests

2 participants