[Agda] Light grey background?

[Jakob von Raumer]

Thanks to all who replied.

I think the light grey is a good choice by the way, it intuitively gave
me the feeling that the definition could be improved even though its
shortcomings weren't dramatic :)

Cheers

Jakob

On 27/04/2020 13:30, Nils Anders Danielsson wrote:
> On 2020-04-26 22:22, Jakob von Raumer wrote:
>> what does light grey background shading mean again?
>
> In Emacs you can find out what the highlighting means by using
> C-u C-x =. Example:
>
>   open import Agda.Builtin.Bool
>
>   f : Bool → Bool → Bool
>   f true  false = false
>   f _     true  = true
>   f false _     = false
>
> If I place the cursor over the first underscore and type C-u C-x =, then
> I get the following output (and more):
>
>   annotation-faces     (agda2-highlight-catchall-clause-face
> agda2-highlight-symbol-face)
>