[Agda] Re: Coloring of mixfix identifiers

Andreas Abel andreas.abel at ifi.lmu.de
Thu Feb 9 13:04:28 CET 2012

Thanks!  Setting the operator face to bold works for me.

It also affects the infix identifiers, though.  Not a big problem.  One 
could think of distinguishing these, but this is a low prio thing.


On 2/9/12 10:58 AM, Nils Anders Danielsson wrote:
> 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".

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de

More information about the Agda mailing list