[Agda] Re: Coloring of mixfix identifiers

[Nils Anders Danielsson]

On 2012-02-07 14:50, Andreas Abel wrote:
> I have a feature request: mixfix-identifiers could receive
> distinguished coloring, to help code comprehension.

This is already implemented, but not activated by default. To activate:

* M-x customize-group RET agda2-highlight RET.

* Go to "Agda2 Highlight Operator Face".

* Configure the face (underlined, maybe).

* Select "State", then "Save for Future Sessions".

-- 
/NAD