[Agda] Sane whitespace with agda --latex

[Mateusz Kowalczyk]

On 04/26/2015 05:20 PM, Andreas Abel wrote:
> As far as I know, to get alignment you need two spaces.
> 
> foo : Bar  x
>             y
>             z
> 
> (Otherwise, how could unintended alignment be ruled out?)
> 
> Cheers,
> Andreas

I tried this and it made no difference. Further, such a hack won't work
for inside let. I end up with having ugly sections like at
http://fuuzetsu.co.uk/images/1430125773.png .

> On 25.04.2015 23:40, Mateusz Kowalczyk wrote:
>> On 04/25/2015 05:46 PM, Mateusz Kowalczyk wrote:
>>> Hi,
>>>
>>> It seems that agda --latex gives a result with horizontal whitespace
>>> that often doesn't resemble the source file. Sometimes things like
>>>
>>> foo : Bar x
>>>            y
>>>            z
>>>
>>> will be turned into
>>>
>>> foo : Bar x
>>>        y
>>>        z
>>>
>>> Sometimes stuff like
>>>
>>> x      : a -> b
>>> longer : a -> b
>>> foo    : a -> b
>>>
>>> Results in some things being properly aligned and others not.
>>>
>>> I even had a case of
>>>
>>> foo : x
>>>      -> let bar : a -> b
>>>       bar = …
>>>         in …
>>>
>>> Is there any way to generate whitespace that's consistent with the
>>> source document? I'm not using tabs or anything like that.
>>>
>>>
>>
>> Peeking into the tex file, we see stuff like (for let case at least)
>>
>>
>> \>[6]\AgdaIndent{10}{}\<[10]%
>> \>[10]\AgdaBound{assoc₂} \AgdaSymbol{:} %rest of line ommited
>> \>          assoc₂ \AgdaSymbol{=} \AgdaFunction{subst⇒₂} %ommited
>>
>> Looks to me like it should be inserting AgdaIndent where it instead
>> inserts regular spaces…
>>
>>
> 
> 


-- 
Mateusz K.