Allow folding of Proofs and Sections

[Arkhist]

VSCoq should allow its users to fold Proof/Qed blocks and Section/End blocks.

I believe this feature should be implemented on the language-server side: implementing it as a language configuration feature could create conflicts between the different block types.

[swils]

I'm only learning Coq, so not an expert, but I'm not convinced that this needs something on the side of the language server. In my personal experience, VSCoq already folds a lot of stuff properly, at least for the simple proofs that I'm currently doing. Could you perhaps send me a couple of snippets that you think cannot be folded properly without the language server?

(By coincidence, the last few days I have been looking at the internals of VSCoq. And perhaps changes to the TextMate definition might allow better folding. Currently everything is in the patterns section; but not much in the repository section. I think (but not sure) that improving this might help with folding. And an unrelated thing that could potentially also be improved is the binding to the scope selectors, spreading it out over more TextMate root groups.)

[Arkhist]

I inspected the source code of the extension and it does seem like all of the folding happening is caused by the auto folding of VSCode itself when using proper indentation.

I am working with libraries that don't start their proof at a different indentation level and in files with more than 2000 lines, folding becomes very useful.

Here is a minimal example where folding doesn't work.

Section test.

Theorem foo: forall a b: Prop, a /\ b -> b /\ a.
Proof.
intros.
split.
destruct H as [Ha Hb].
exact Hb.
destruct H as [Ha Hb].
exact Ha.
Qed.

Theorem bar: forall a b: Prop, a \/ b -> b \/ a.
Proof.
intros.
destruct H.
right.
assumption.
left.
assumption.
Qed.

End test.

[TheoWinterhalter]

Note that Proof is not mandatory at the beginning of a proof, which might make folding harder.

[swils]

No @Arkhist you're right. Improving the TextMate file does not improve the folding. Too bad...

[Blaisorblade]

I share @Arkhist's experience.

Note that Proof is not mandatory at the beginning of a proof, which might make folding harder.

Omitting Proof is problematic for other reasons, so only folding proofs that start with Proof could already help.

[TheoWinterhalter]

You're right.