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

[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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: STLC.agda
Type: application/octet-stream
Size: 13452 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190201/f7bf9ea6/attachment.obj>