[Agda] Sane whitespace with agda --latex

[Mateusz Kowalczyk]

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.