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

On Tue, Apr 12, 2011 at 5:38 AM, Christoph Sprenger
<sprenger at> wrote:
> Hi,
> I have recently installed the Isabelle 2011 on Mac Application, which
> includes
>  Carbon Emacs 23.2, and
>  ProofGeneral 4.1pre101216
> 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.

I also have a related-but-different problem with delete vs. backspace
in the same version of ProofGeneral, but on Linux (Ubuntu) with GNU
Emacs 23.2.1. The delete key normally works properly, doing
forward-delete; but the symbol input shortcuts cause problems. For
example, if I have just typed "-" or "--" (which are prefixes of
"-->", the shortcut for the \<longrightarrow> symbol), then my
"delete" key works like "backspace" instead.

Interestingly, Carbon Emacs seems to do the right thing in this
situation once I have "normal-erase-is-backspace" set properly, but
GNU Emacs on Linux gets it wrong no matter how
"normal-erase-is-backspace" is set.

> 3) When I point the mouse on a processed part of the input it becomes
> highlighted in yellow and displays a "tooltip" frame with info about the
> underlying object. Inside proofs it shows the proof state at the mouse
> position. While this looks like a cool new feature in PG4, I would like to
> be able to turn both the highlighting and the "tooltips" off, when I do not
> need them. However, I was unable to find an option that achieves this.

I would also like to be able to turn this feature off.

- Brian

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