<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
Hi Marko,<br>
<div><br>
</div>
<div>Maybe commenting with '--' could be a temporary workaround? Prepending '-- ' to every line in an emacs buffer (assuming evil mode) should only take a few keystrokes, and can be made into a macro (and same for uncommenting). It might prevent Agda from interpretting
triple backtics as the end of comments.<br>
</div>
<div><br>
</div>
<div>Hope it helps,</div>
<div><br>
</div>
<div>
<div></div>
<div></div>
<div></div>
<div><span></span><span>Uma</span></div>
<div><span><br>
</span></div>
<div><span>---<br>
</span></div>
<div><span>pronoun: she<br>
</span></div>
<div><span>website: umazalakain.info</span></div>
<div>twitter: @typer_uma</div>
<div>desk: SAWB F112<br>
</div>
<div></div>
</div>
<div><br>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size: 11pt; --darkreader-inline-color:#e8e6e3;" data-darkreader-inline-color="" face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Marko Dimjašević <marko@dimjasevic.net><br>
<b>Sent:</b> 11 September 2020 14:01<br>
<b>To:</b> Jesper Cockx <Jesper@sikanda.be><br>
<b>Cc:</b> agda list <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] Multi-line comments in literate Agda files</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Hi Jesper,<br>
<br>
On Fri, 2020-09-11 at 09:45 +0200, Jesper Cockx wrote:<br>
> Hi Marko,<br>
> <br>
> I believe the literal Agda mode *only* looks at the parts between the<br>
> begin- and end-code markers (in this case ```). This includes begin- and<br>
> end-comment markers, so in this case they are ignored. One trick you<br>
> could use is to put some text immediately after the first triple<br>
> backtick, which will cause Agda to ignore the whole block. E.g.<br>
> <br>
> ```ignore<br>
> count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p<br>
> count {_ , _} zero _ = Z<br>
> count {Γ , _} (suc n) (s≤s p) = S (count n p)<br>
> ```<br>
<br>
<br>
Thanks for the pointer, but my hope was I can comment out half a file in<br>
one stroke, and this isn't it as there are lots of code blocks I'd have to<br>
invalidate in isolation per your suggestion.<br>
<br>
For now I'm copying the relevant definitions into a separate self-contained <br>
file/buffer and type-checking that until it is done, and then I copy back<br>
to the original literate Agda file the updates I just made in the separate<br>
buffer. It ain't the best experience, but it is faster than type-checking<br>
the whole literate file.<br>
<br>
<br>
--<br>
Cheers,<br>
Marko<br>
<br>
</div>
</span></font></div>
</body>
</html>