[Agda] Re: Coloring of mixfix identifiers

Stefan Monnier monnier at iro.umontreal.ca
Wed Feb 8 17:55:12 CET 2012


> Emacs has a feature to highlight a parenthesis corresponding to the
> one at the cursor. Highlighting the corresponding portions of a mixfix
> operator would be a natural, useful extension.

I agree with Andreas that highlighting is an orthogonal issue.
But while I'm here: Emacs-23.3 introduced SMIE (a generic indentation
and navigation engine) and Emacs-24 uses it when available to match
keywords like you describe.  SMIE relies on operator precedence parsing,
which is close enough to Agda's parsing technology that it should be
possible to make Agda mode use SMIE.  The main problem would be how to
make SMIE understand the layout rules and how to figure out which mixfix
are in scope.


        Stefan



More information about the Agda mailing list