[Agda] agda --latex inline code

[Altenkirch Thorsten]

On 12/05/2014 12:43, "Stevan Andjelkovic"
<stevan.andjelkovic at strath.ac.uk> wrote:

>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).

Maybe what I am suggesting is to integrate lhs2tex into Agda, instead
having two tools with overlapping functionality.

Thorsten

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.