[Agda] Orange highlights in EMACS Agda mode

[Roly Perera]

Hi,

I've been using Agda for a few weeks but have only recently
encountered the orange highlighting in the EMACS mode.  I'm remember
reading about it somewhere but I can't find any mention of it now in
the documentation, on the Wiki or by searching the mailing list
archives.

I'm sure it's something basic.  It seems to have arisen since I
started developing a largish mutually recursive definition in a
stepwise fashion by introducing postulates for some of the functions
which will be eventually be defined in the mutual block (not sure if
that is a legitimate way to proceed anyway, but that's another
question).  Some things are now highlighted in orange but no actual
message comes back from the Agda compiler, so I've no idea what it
means.  Could someone please clarify?

thanks,
Roly