[Agda] Multi-line comments in literate Agda files

[Uma Zalakain (PGR)]

Hi Marko,

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.

Hope it helps,

Uma

---
pronoun: she
website: umazalakain.info
twitter: @typer_uma
desk: SAWB F112

________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Marko Dimjašević <marko at dimjasevic.net>
Sent: 11 September 2020 14:01
To: Jesper Cockx <Jesper at sikanda.be>
Cc: agda list <agda at lists.chalmers.se>
Subject: Re: [Agda] Multi-line comments in literate Agda files

Hi Jesper,

On Fri, 2020-09-11 at 09:45 +0200, Jesper Cockx wrote:
> Hi Marko,
>
> I believe the literal Agda mode *only* looks at the parts between the
> begin- and end-code markers (in this case ```). This includes begin- and
> end-comment markers, so in this case they are ignored. One trick you
> could use is to put some text immediately after the first triple
> backtick, which will cause Agda to ignore the whole block. E.g.
>
> ```ignore
> count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p
> count {_ , _} zero _     =  Z
> count {Γ , _} (suc n) (s≤s p)  =  S (count n p)
> ```


Thanks for the pointer, but my hope was I can comment out half a file in
one stroke, and this isn't it as there are lots of code blocks I'd have to
invalidate in isolation per your suggestion.

For now I'm copying the relevant definitions into a separate self-contained
file/buffer and type-checking that until it is done, and then I copy back
to the original literate Agda file the updates I just made in the separate
buffer. It ain't the best experience, but it is faster than type-checking
the whole literate file.


--
Cheers,
Marko

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200911/580f00f0/attachment.html>