[Agda] lhs2TeX-1.14 with Agda support

[Nils Anders Danielsson]

On 24/10/08 11:15, Andres Loeh wrote:
> 
> I've just released lhs2TeX-1.14 with experimental support for Agda.
> I'm aware that a lot more can be done (for instance have Agda itself
> provide formatting information that can be read by lhs2TeX, much like
> it provides highlighting information for Emacs right now), but this is
> at least a start.

Nice, I have already started using the new version.

Can you describe the new lexing algorithm? Is everything treated as an
ordinary identifier (as opposed to an infix operator)?

Since Agda does not distinguish constructors and other functions
lexically I would recommend people to change the highlighting of
constructors manually, using format directives:

   %format true "\constructor{true}"

(For a suitable definition of \constructor, I usually use \mathsf.)

It would indeed be nice if lhs2TeX could make use of the information
present in Agda. Values of the type
Agda.Interaction.Highlighting.Precise.File represent the highlighting
information available for a given file. Is this representation suitable
for lhs2TeX? (I suppose defining an external, reusable format for
highlighting information would be a good idea.)

-- 
/NAD

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.