<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
There are lots of similar tools. One alternative is packages that allows you to hide some marked regions, e.g.
<a href="https://www.emacswiki.org/emacs/HideRegion" id="LPNoLP700434">https://www.emacswiki.org/emacs/HideRegion</a><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
but tools like this tend to pollute the source code by markers that do not contribute to the content of the code.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Pierre-Evariste Dagand <pedagand@gmail.com><br>
<b>Sent:</b> February 1, 2019 11:01 AM<br>
<b>To:</b> Erik Palmgren<br>
<b>Cc:</b> Agda@lists.chalmers.se<br>
<b>Subject:</b> Re: [Agda] Hiding parts of proofs in Emacs Agda mode?</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">> Does any know if there is some way of temporarily hiding parts of proofs in<br>
> Emacs Agda mode? Maybe some general feature of Emacs can do that?<br>
<br>
You're looking for outline-minor-mode<br>
[<a href="https://www.emacswiki.org/emacs/OutlineMinorMode">https://www.emacswiki.org/emacs/OutlineMinorMode</a>]. Attached is a<br>
(decade old) example using this (type 'y' when emacs asks about<br>
setting local variables).<br>
<br>
Here is some convenient navigation hooks (to put in your .emacs.el):<br>
<br>
(add-hook 'outline-minor-mode-hook<br>
(lambda ()<br>
(define-key outline-minor-mode-map [(control tab)] 'org-cycle)<br>
(define-key outline-minor-mode-map [(backtab)] 'org-global-cycle)<br>
(define-key outline-minor-mode-map [M-up] 'outline-backward-same-level)<br>
(define-key outline-minor-mode-map [M-down] 'outline-forward-same-level)<br>
(define-key outline-minor-mode-map [M-left] 'outline-up-heading)<br>
(define-key outline-minor-mode-map [M-right]<br>
'outline-next-visible-heading)))<br>
<br>
--<br>
Pierre<br>
</div>
</span></font></div>
</body>
</html>