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

[Martin Escardo]

It would also be nice if the agda --html command-line option had a 
sub-option to "fold" definitions, with something to click to open them.

Apparently you do this with <summary> and <details> in html.

This could also already work for literate code using markdown, but I 
haven't tried it.

Martin

On 01/02/2019 14:43, guillaume.brunerie at gmail.com wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe