Improving code folding

Stream: lean4

[Bhavik Mehta]

It would be really nice if code folding allowed me to fold away the proof of a theorem, so I can scroll through my file and see what I've proved. In addition, folding away the proofs of subgoals (even if only ones started by have _ : _ := by) would be super helpful. Having the list of names in the explorer tab is nice, but statements are clearly more valuable than just names!

[Kim Morrison]

Do you mean that you want code folding to start at the := rather than just after the first line?

[Kevin Buzzard]

I just tried folding a lemma I was looking at in a random file

@[simp, norm_cast]
lemma add_apply (φ ψ : AutomorphicForm F D M) (x : (D ⊗[F] (FiniteAdeleRing (𝓞 F) F))ˣ) :
    (φ + ψ) x = (φ x) + (ψ x) := rfl

and it folds away everything apart from the attribute line :-)

[Daniel Weber]

It also folds the empty line after the lemma which looks weird

[Bhavik Mehta]

Kim Morrison said:

Do you mean that you want code folding to start at the := rather than just after the first line?

If I'm understanding your meaning correctly, yes. And I'd like the fold to end on the same line that contains the last line of the proof. And the same rule for have/obtain _ : _ := blocks

[Kim Morrison]

We're constrained here by what the code folding API provided by VSCode allows (and I certainly don't know the details). If someone interested in this wanted to do that research...?

[Julian Berman]

Not that I know everything inside and out, but this is the LSP method: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_foldingRange
I think the first thing to consider is whether setting collapsedText already gets things nice enough (that's the text shown when folded, so one could set it to the type and leave everything else as is without even changing the range -- I don't know for sure that VSCode supports that field but it seems likely and verifiable that it does).
Adding additional ranges for have I think would be a second bit.

[Julian Berman]

This is the server side: https://github.com/leanprover/lean4/blob/21d71de481e3d497a3ceeac85e50b50338b5636d/src/Lean/Server/FileWorker/RequestHandling.lean#L594 -- so probably staring at that is where testing such a change would go I think. If no one else volunteers I can have a closer look though I don't know off hand what thing available there has the type information for what's being folded, if anything.

[Marc Huisinga]

Please make an RFC. I have been neglecting this feature a bit because I wasn't aware that it was seeing lots of usage.

[Mario Carneiro]

It's definitely possible to make a code action cover whatever span of text you want

[Mario Carneiro]

the pattern match code action does exactly that:

def foo : Inhabited Nat := _
                        -- ^ generate a skeleton for the structure under construction

def foo : Inhabited Nat where
  default := _

[Mario Carneiro]

note that the := was deleted even though it is not in the span of the _

[Mario Carneiro]

oh whoops I got my lines crossed, this is about folding regions not code actions

[Mario Carneiro]

folding regions are constrained in the UX to be full lines

[Mario Carneiro]

I think the LSP protocol itself allows more but vscode can't do much with intra-line information