[Agda] Re: Coloring of mixfix identifiers

[Stefan Monnier]

> 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