[Agda] literate colours

gallais guillaume.allais at ens-lyon.org
Mon May 18 13:55:04 CEST 2015


This is inherent to the way html is displayed I believe. You can use the
pre attribute to have the browser respect your formatting:
http://www.w3schools.com/cssref/pr_text_white-space.asp

On 16/05/15 12:46, Mateusz Kowalczyk wrote:
> 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?
>



More information about the Agda mailing list