[Agda] Hiding parts of proofs in Emacs Agda mode?

[Guillaume Brunerie]

Apparently there is also a minor mode for emacs which does folding
based on indentation: https://github.com/zenozeng/yafolding.el.
I haven’t tried it, so I don’t know if it actually works with Agda.

There is also Folding mode
(https://www.emacswiki.org/emacs/FoldingMode), but it requires quite
ugly {{{ and }}} markers (although they might be customizable).

Best,
Guillaume

Den fre 1 feb. 2019 kl 15:32 skrev Jonathan Steven Prieto Cubides
<Jonathan.Cubides at uib.no>:
>
> Hi Erik,
>
>
> If you use the Atom editor and the add-on Agda Mode, that's
>
> what you want is possible. Just use indentation if you want to hide
>
> parts of the code. Atom allows you to fold or unfold all the code
>
> at some level of indentation.
>
>
> https://github.com/banacorn/agda-mode
>
>
> Jonathan
>
> ________________________________
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Erik Palmgren <palmgren at math.su.se>
> Sent: Friday, February 1, 2019 11:47:13 AM
> To: Agda at lists.chalmers.se
> Subject: [Agda] Hiding parts of proofs in Emacs Agda mode?
>
>
>
> Does any know if there is some way of temporarily hiding parts of proofs in
>
> Emacs Agda mode? Maybe some general feature of Emacs can do that?
>
>
> For instance, it would be useful to hide definiens/proofs when browsing
>
> Agda files.
>
>
> I seem to recall that there was such a feature in Alfa a GUI for Agda 1, which
>
> was very useful . In e.g. Mathematica there is also a convenient section system,
>
> where parts can be hidden or folded away with a click.
>
>
>
> Erik
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda