[Agda] agda --latex inline code

[Nils Anders Danielsson]

On 2014-05-12 13:43, Stevan Andjelkovic wrote:
> 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).

Most of the (non-interactive) highlighting information only requires
scope-checking, not type-checking. Perhaps it wouldn't be too hard to
rewire Agda so that scope-based highlighting information can be produced
for inline code and spec blocks.

-- 
/NAD