[Agda] literate colours

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Sat May 16 13:46:47 CEST 2015


On 05/15/2015 08:47 PM, Martin Escardo wrote:
> In a literate Agda file when rendered with agda --html, the comments are
> red.
> 
> But in the way I use literate Agda, the comments are the substance and
> the code is the form of the substance.
> 
> The substance shouldn't be red - plain black would work better with me.
> 
> How can I change the colours of the substance and the form?
> 
> Thanks,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

While we're complaining about comments in literate output, is there a
reason why the spaces between words are not rendered in comments?

-- 
Mateusz K.


More information about the Agda mailing list