[Agda] Agda and Aquamacs
Nils Anders Danielsson
nils.anders.danielsson at gmail.com
Thu Jun 19 14:39:19 CEST 2008
On Thu, Jun 19, 2008 at 7:14 AM, Sean Leather <sean.leather at gmail.com> wrote:
>
> On Thu, Jun 19, 2008 at 02:43, WILSON F.A.J. <frank.wilson at durham.ac.uk>
> wrote:
>>
>> (Given Monaco is your default font, it should
>> not need to be changed when loading agda files since it should
>> have all the glyphs. I think....)
>
> Yes, Monaco has all of the Unicode characters I've needed so far.
If Monaco can handle most of the characters used in the standard
library, and is installed by default under MacOS, then we should make
it the default for Agda under MacOS. If this is the case, can some
Mac-user update agda2-mode.el?
The reason for changing the default font of the current frame when the
Agda mode is started is to ensure that a decent font with good support
for Unicode symbols is used. However, no one has provided a default
setting for Macs yet.
--
/NAD
More information about the Agda
mailing list