[Agda] Agda and Aquamacs

[Sean Leather]

Hi,

I'm using Aquamacs[1], an Emacs derivative, on the Mac to work with Agda.
I've tried just about every possible graphical Emacs option available, and
Aquamacs seems to work the best. It's a nice editor (excluding the fact that
I'm not an Emacs user), but I'm having at least one annoying problem with
it.

I have set the default font to 12-pt Monaco. Suppose I have a window X with
some file (it doesn't matter what) open in Aquamacs. Then, I open an Agda
file in a new window Y. The text of window X changes to a proportional (not
fixed-pitch) font (Abadi MT Condensed Extra Bold, which happens to be first
in the list, alphabetically). The text in Y is Monaco as I would expect. If
I open a non-Agda file in Y instead, the font of X does not change.

I know at least one other person who has the exact same problem. Has anybody
else seen this and/or figured out how to fix it?

Thanks,
Sean

[WILSON F.A.J.]

In the options group (M-x customize-group RET agda2 RET)
have you tried setting "Change Default Font" to "Don't change"?
I could be wrong, but I think this will get rid of the behaviour
you are describing. (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....)

Frank



-----Original Message-----
From: agda-***@lists.chalmers.se on behalf of Sean Leather
Sent: Wed 18/06/2008 22:37
To: Agda List
Subject: [Agda] Agda and Aquamacs

Hi,

I'm using Aquamacs[1], an Emacs derivative, on the Mac to work with Agda.
I've tried just about every possible graphical Emacs option available, and
Aquamacs seems to work the best. It's a nice editor (excluding the fact that
I'm not an Emacs user), but I'm having at least one annoying problem with
it.

I have set the default font to 12-pt Monaco. Suppose I have a window X with
some file (it doesn't matter what) open in Aquamacs. Then, I open an Agda
file in a new window Y. The text of window X changes to a proportional (not
fixed-pitch) font (Abadi MT Condensed Extra Bold, which happens to be first
in the list, alphabetically). The text in Y is Monaco as I would expect. If
I open a non-Agda file in Y instead, the font of X does not change.

I know at least one other person who has the exact same problem. Has anybody
else seen this and/or figured out how to fix it?

Thanks,
Sean

[Sean Leather]

Hi,

Post by WILSON F.A.J.
In the options group (M-x customize-group RET agda2 RET)
have you tried setting "Change Default Font" to "Don't change"?
I could be wrong, but I think this will get rid of the behaviour
you are describing.

That worked! It's now so much nicer to play with Agda. :)

Post by WILSON F.A.J.
(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.

Thanks,
Sean

[Nils Anders Danielsson]

Post by Sean Leather

Post by WILSON F.A.J.
(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.

[Sean Leather]

Hi,

On Thu, Jun 19, 2008 at 14:39, Nils Anders Danielsson <

Post by Nils Anders Danielsson
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?

I would be happy to help; however, I am not at all familiar with Emacs, let
alone Elisp. I see the following lines in agda2-mode.el

(defcustom agda2-fontset-spec
(concat
"-misc-fixed-medium-r-normal-*-15-*-*-*-*-*-fontset-agda2"
(cond
((eq window-system 'w32) ",
ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1,
...

with a list of other fonts that follow. So, I'm guessing one needs to add
another condition for Mac, but I don't quite know how.

If you give me a pointer in a direction to go, I'll try something.
Otherwise, I'll test changes.

The reason for changing the default font of the current frame when the

Post by Nils Anders Danielsson
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.

Perhaps I'm missing something, but why is it that the frame that loses focus
change to another font? The frame that opens with the new file does open
with my default font.

Sean

[Nils Anders Danielsson]

Post by Sean Leather
I would be happy to help; however, I am not at all familiar with Emacs, let
alone Elisp. I see the following lines in agda2-mode.el
(defcustom agda2-fontset-spec
(concat
"-misc-fixed-medium-r-normal-*-15-*-*-*-*-*-fontset-agda2"
(cond
((eq window-system 'w32) ",
ascii:-Misc-Fixed-Medium-R-Normal--15-140-75-75-C-90-ISO8859-1,
...
with a list of other fonts that follow. So, I'm guessing one needs to add
another condition for Mac

Yes. You can experiment by customising agda2-fontset-spec (M-x
customize-group agda2). However, I'm not sure that you can specify the
Monaco font using such fontsets. Maybe some Aquamacs user can comment
on this.

Post by Sean Leather
Perhaps I'm missing something, but why is it that the frame that loses focus
change to another font? The frame that opens with the new file does open
with my default font.

Perhaps the new frame has not been created when the Agda mode is
started. Try opening the frame first, before opening the Agda file
(C-x 5 2 C-x C-f).

[Sean Leather]

Hi,

Thanks for all the responses!

Post by Sean Leather
Perhaps I'm missing something, but why is it that the frame that loses focus

Post by Sean Leather
change to another font? The frame that opens with the new file does open
with my default font.

Perhaps the new frame has not been created when the Agda mode is
started. Try opening the frame first, before opening the Agda file
(C-x 5 2 C-x C-f).

This does work around the problem. I did that before learning about the
"change default" setting. It added an extra step to opening every file, and
that's what sparked my initial question.

This might be an Aquamacs peculiarity. Try adding this line to your

Post by Sean Leather
~/Library/Preferences/Aquamacs Emacs/Preferences.el
'(one-buffer-one-frame-mode nil nil (aquamacs-frame-setup))
This shouldn't open a new window for every buffer. It might fix your
problem together with '(agda2-change-default-font nil).

Yes, this is another workaround; however, I decided that I liked having
multiple windows open.

Sean

[Nils Anders Danielsson]

Post by Sean Leather
This does work around the problem. I did that before learning about the
"change default" setting. It added an extra step to opening every file, and
that's what sparked my initial question.

It is arguably bad behaviour for the Agda mode to change the frame's
default font (hence the agda2-change-default-font setting). I still
think it is useful to do this, though, since the default default font
is often inadequate. Maybe someone more Emacs-savvy knows a better way
to accomplish our goals?

[Wouter Swierstra]

Post by Sean Leather
Perhaps I'm missing something, but why is it that the frame that
loses focus change to another font? The frame that opens with the
new file does open with my default font.

This might be an Aquamacs peculiarity. Try adding this line to your ~/
Library/Preferences/Aquamacs Emacs/Preferences.el

'(one-buffer-one-frame-mode nil nil (aquamacs-frame-setup))

This shouldn't open a new window for every buffer. It might fix your
problem together with '(agda2-change-default-font nil).

Hope this helps,

Wouter


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.