[isabelle] Emacs 23/PG 4 problems on Mac



Hi,

I have recently installed the Isabelle 2011 on Mac Application, which includes

  Carbon Emacs 23.2, and
  ProofGeneral 4.1pre101216

(before I was using Isabelle 2009-1 with CE 22.3 and PG 3.7.1.1). There a number of "features" of this combo that tend to drive me nuts. These are:

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

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 sentence, - 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 very often.

I would greatly appreciate any help with these issues.

Best wishes,
Christoph








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