[Agda] literate colours

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Mon May 18 15:32:21 CEST 2015


On 05/18/2015 12:55 PM, gallais wrote:
> 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

Oh, damn, seems I was half asleep and didn't realise this was about
--html and not --latex… Oops.

> 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
>>> _______________________________________________



-- 
Mateusz K.


More information about the Agda mailing list