[Agda] Multi-line comments in literate Agda files

[Marko Dimjašević]

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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200911/5c60a5a5/attachment.sig>