[isabelle] Emacs 23/PG 4 problems on Mac
I have recently installed the Isabelle 2011 on Mac Application, which
Carbon Emacs 23.2, and
(before I was using Isabelle 2009-1 with CE 22.3 and PG 126.96.36.199).
There a number of "features" of this combo that tend to drive me nuts.
1) The Emacs Meta modifier is bound to the Option key instead of the
2) The Delete key acts like Backspace.
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.
4) There seem to be some bugs in PG 4 by which
- the command processing gets out of sync (previously rare), indicated
by the highlighting ending in the middle of a syntactic token or input
- the highlighting is not properly removed and some bits of processed
input stay yellow, after the mouse is moved away.
1) and 2) seem to be PG-independent "features" of CE 23.2 (does my CE
22 config possibly disturb CE 23?), while 3) and 4) are PG-specific.
Point 4) is less of a problem than the others, since it does not occur
I would greatly appreciate any help with these issues.
This archive was generated by a fusion of
Pipermail (Mailman edition) and