[Agda] lhs2TeX-1.14 with Agda support

[Andres Loeh]

Hi.

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

Glad you like it :)

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

Informally:

* Agda's list of keywords is recognised.
* I've tried to reproduce Agda's rules for separating tokens from
  each other (i.e., only a very small list of symbols and spaces
  separate tokens, quite different from Haskell).
* There's no distinction between operators and identifiers.

If you find things that don't work as expected, please let me know.
I haven't tested this very thoroughly yet.

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

Yes. It'd also be nice to distinguish local identifiers from
global identifiers, for instance.

Other things on the TODO list:

* Define more Unicode symbols.
* Somehow allow specifying formatting directives for mixfix operators.

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

I'll have a look sometime soon.

Cheers,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
http://www.andres-loeh.de