[Agda] Font Problems on Mac OS X

[Shin-Cheng Mu]

Hi,

I have been running Agda and its Emacs mode on my OS X for a while.
The version I was running was probably checked out from the dracs
repository a month ago. I thought OS X is relatively UTF-8 ready,
but it appears that some characters are still missing in the fonts.
For example, the semantic brackets in AIM6/RegExp/SimpleMatcher.agda.

Today I checked out the latest Agda 2 source today and tried to re- 
install
the Emacs mode. I was given following error message while loading
an Agda file into Emacs:

   File mode specification error:
     (error "Font `fontset-agda2' is not defined")

So I opened agda2-mode.el and added

     ((eq window-system 'mac) "")

after

     ((eq window-system 'x) "")

on line 122, and changed line 167 to

     (if (memq window-system '(x w32 mac))

I am not sure whether I did the right thing, but the error message
was gone anyway.

However, after loading a file, Emacs switched to a font different
from the usual "Monaco". It was a very narrow font not comfortable to
read, so I eventually changed the "Agda2 Change Default Font"
option to "Don't Change."

So... does anyone know where I can find the right fonts for
OS X, and how to install them?

Thanks!

sincerely,
Shin