[Agda] permanently changing the Agda font

[J.Burton at brighton.ac.uk]

At Tue, 15 Sep 2009 15:37:26 +0200,
Wolfgang Jeltsch wrote:
> 
> 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. ;-) )
>

Hi, I meant the darcs version of agda2-mode. You can use it without
using the development version of agda. Get the agda repo with the
instructions on the wiki into, say, ~/agda, then add something like
this in .emacs:

;; remove stuff about agda-mode locate & 
;; use the dev version of agda2-mode
(add-to-list 'load-path (expand-file-name "~/agda/Agda/src/data/emacs-mode"))
(require 'agda2)

> 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?
>

The simplest way is to wait til that change is in a release. Any other
way would be messier than temporarily using the dev version of agda2-mode.

Jim

> Best wishes,
> Wolfgang
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda