[Agda] permanently changing the Agda font

[Wolfgang Jeltsch]

Am Dienstag, 15. September 2009 14:42:02 schrieben Sie:
> At Tue, 15 Sep 2009 12:54:33 +0200,
>
> Wolfgang Jeltsch wrote:
> > Hello,
> >
> > I have changed the default font of Emacs and stored this setting in my
> > ~/.emacs file. When I restart Emacs, this font is used. However, when I
> > open an Agda buffer, Agda overrules my decision. How can I permanently
> > change the font for Agda?
>
> Hi, if you use the darcs emacs-mode you can customize the group, edit
> Agda2 Highlight Face Groups and select "Use simplified highlighting
> and default font-lock faces." Saving this choice edits your init file
> and agda-mode will use your default fonts and colour theme.

Hi,

what is the darcs emacs-mode? The darcs version of Agda’s Emacs mode? (I 
wondered whether you meant an Emacs mode for darcs. ;-) )

I use the latest stable version of Agda, so your suggestion doesn’t help me, 
alas. I could live without Agda using the default font of Emacs. However, it 
must be possible to separately change also the font of Agda. How can this be 
done?

Best wishes,
Wolfgang