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

[Erik Palmgren]

Many thanks for this solution and the nice Agda example.
I will try this out, and in particular how navigation
works in Aquamacs.

Thanks also for the other responses. Good to know about
an alternative Agda editor.

Erik


Den 2019-02-01 kl. 17:01, skrev Pierre-Evariste Dagand:
>> 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?
> 
> You're looking for outline-minor-mode
> [https://www.emacswiki.org/emacs/OutlineMinorMode]. Attached is a
> (decade old) example using this (type 'y' when emacs asks about
> setting local variables).
> 
> Here is some convenient navigation hooks (to put in your .emacs.el):
> 
> (add-hook 'outline-minor-mode-hook
>    (lambda ()
>      (define-key outline-minor-mode-map [(control tab)] 'org-cycle)
>      (define-key outline-minor-mode-map [(backtab)] 'org-global-cycle)
>      (define-key outline-minor-mode-map [M-up] 'outline-backward-same-level)
>      (define-key outline-minor-mode-map [M-down] 
> 'outline-forward-same-level)
>      (define-key outline-minor-mode-map [M-left] 'outline-up-heading)
>      (define-key outline-minor-mode-map [M-right]
> 'outline-next-visible-heading)))
> 
> --
> Pierre