Code folding in language server

Stream: lean4

[Jonathan Coates]

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]

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.