Re: [isabelle] Emacs 23/PG 4 problems on Mac

Dear Brian and Makarius,

thank you for your helpful suggestions regarding the Emacs-specific problems 1) and 2).

@Brian regarding backspace problem:
Setting normal-erase-is-backspace to On solves my problem.

@Makarius regarding modifier keys:
Your command switches off the interpretation of the Option key by Emacs, which is good. But I also and had to set mac-command-modifier to meta in order to restore things to "normal". I did this via the menus, so my .emacs now contains

 '(ns-alternate-modifier (quote none))
 '(ns-command-modifier (quote meta))

Here, ... denotes other settings and "ns-command-modifier" is a synonym for "mac-command-modifier" and similarly for the other.


On 13 Apr 2011, at 10:13, Makarius wrote:

On Tue, 12 Apr 2011, Christoph Sprenger wrote:

1) The Emacs Meta modifier is bound to the Option key instead of the Command key.

I have something like this in my $ISABELLE_HOME_USER/etc/ proofgeneral-settings.el, but you can also use the customization menu in Emacs:

  (setq mac-option-modifier nil)


On 12 Apr 2011, at 18:52, Brian Huffman wrote:

2) The Delete key acts like Backspace.

This one at least is not too hard to fix. You will need to customize
the option "normal-erase-is-backspace", which you can do using

Options > Customize Emacs > Specific Option...

and typing in "normal-erase-is-backspace". Try setting the value to
"On", and see if this solves your problem.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.