[Agda] Sane whitespace with agda --latex

[Andreas Abel]

For an example of literate Agda code processed by agda --latex,
see

   http://www.cse.chalmers.se/~abela/msfp14.lagda

On 27.04.2015 16:06, Wolfram Kahl wrote:
> On Mon, Apr 27, 2015 at 10:10:42AM +0100, Mateusz Kowalczyk wrote:
>> 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?)
>>
>> I tried this and it made no difference. Further, such a hack won't work
>> for inside let.
>
> That would be another reason to stick with lhs2TeX:
>
>     http://www.andres-loeh.de/lhs2tex/
>
> (Reading the manual is necessary. The two-space rule essentially
>   comes from there. With my Emacs setup, Unicode characters like
>   suffix _1 etc. do not have the same width as other characters,
>   so frequently it is necessary to look at the column numbers
>   in the status bar to be able to actually achieve alignment.)
>
> My main reason to not even consider ``agda --latex'' right now
> is that, as far as I know (and I do read Agda release notes),
> it does not typeset in-line code (as in ``|sym D.Laws A.assoc|'').
> I find that even a minimal degree of literacy is hard to achieve
> without the facility to typeset in-line code.
>
>
>> I end up with having ugly sections like at
>> http://fuuzetsu.co.uk/images/1430125773.png .
>
> (Too much is missing from that picture to even guess what you might
>   want to point to.)
>
>
>
> Wolfram
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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