Zulip Chat Archive

Stream: lean4

Topic: Code folding in language server


Jonathan Coates (Feb 10 2022 at 20:58):

Just wondering if there's any plans to support LSP's folding ranges (https://microsoft.github.io/language-server-protocol/specifications/specification-current/#textDocument_foldingRange) within the language server? It feels like it might be useful for some constructs which don't use indentation (section, namespace), but also no clue how practical it is with Lean's parsing/syntax system.

Henrik Böving (Feb 10 2022 at 21:01):

All declarations are associated with a line range in the file so it should certainly be possible to implement some folding for those, maybe you can open an issue on Github about it.


Last updated: Dec 20 2023 at 11:08 UTC