[Agda] aquamacs gremlins
Nils Anders Danielsson
nils.anders.danielsson at gmail.com
Fri Feb 29 23:43:52 CET 2008
On Fri, Feb 29, 2008 at 5:30 PM, Conor McBride
<conor at strictlypositive.org> wrote:
>
> But now when I load an agda file, I get no colours
> (or other useful functionality) and the message...
>
> File mode specification error: (error "Font `fontset-agda2' is not
> defined")
Easy solution: Make sure that the Agda mode does not try to change
your default font (M-x customize-variable agda2-change-default-font).
Better solution: Apply the attached bugfix patch. You probably need to
change agda2-fontset-spec, though (M-x customize-variable
agda2-fontset-spec).
Agda tries to change your default font in order to ensure good support
for Unicode characters, but no one has provided us with reasonable
settings which work under the Mac window system. If you find a nice
setting of agda2-fontset-spec, then please tell us. Alternatively, if
things work nicely out of the box (with agda2-change-default-font set
to nil), tell us so that we can make sure that the font settings are
not touched on Macs.
--
/NAD
-------------- next part --------------
A non-text attachment was scrubbed...
Name: font-fix.patch
Type: text/x-patch
Size: 28835 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080229/47380d1d/font-fix-0001.bin
More information about the Agda
mailing list