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

[Jason -Zhong Sheng- Hu]

There are lots of similar tools. One alternative is packages that allows you to hide some marked regions, e.g. https://www.emacswiki.org/emacs/HideRegion
but tools like this tend to pollute the source code by markers that do not contribute to the content of the code.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Pierre-Evariste Dagand <pedagand at gmail.com>
Sent: February 1, 2019 11:01 AM
To: Erik Palmgren
Cc: Agda at lists.chalmers.se
Subject: Re: [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?

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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190201/58410503/attachment.html>