how is folding handled?

Stream: lean4

[Eric Rodriguez]

I notice that there is some LSP commands for folding, but I was also trying to mess around with VSCode and it seems to me that any sort of folding is indentation-based; is the truth a mix?

Context: I'm looking at making commands like says autofold (i.e. when we have simp? says simp only [.....] we can just show simp? <folded> or the equivalent) to encourage more use of them, and I'm trying to slowly get my head round LSP, Lean's implementation of it, and how VSCode deals with the responses all at the same time

[Sebastian Ullrich]

The implementation in Lean is based on the syntax tree structure but I can't tell you what VS Code does with that result

[Sebastian Ullrich]

In theory, it should be possible to add your own logic via chainLspRequestHandler