[Agda] agda --latex inline code

[Stevan Andjelkovic]

On Sat, May 10, 2014 at 02:29:03PM +0100, Altenkirch Thorsten wrote:
>
> Would it be possible to fix that? I mean it would be nice to have the
> inline functionality of lhs2tex.

Probably, but not easily. It has been proposed and discussed this in
the past, see:

  https://code.google.com/p/agda/issues/detail?id=1054

> >Typechecking is essential to the typesetting (otherwise we don't
> >know what colours etc to use).
> 
> Yes, I realize that. Maybe it would be possible only to use the parser for
> inline code and spec-blocks? For monochrome output?

The backend is using the highlighting info (basically a list of tokens
with attributes) produced by the typechecker, and all it does is to
translate those into appropriate latex commands.

It would be possible to use the output of the parser as a basis for
the latex output instead, but this would be an entirely different
program (largely duplicating the work of lhs2tex).