[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