[Agda] Sane whitespace with agda --latex

[Andreas Abel]

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

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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/