[Agda] Re: Coloring of mixfix identifiers

[Andreas Abel]

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.

Cheers,
Andreas

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
http://www2.tcs.ifi.lmu.de/~abel/