[isabelle-dev] Proof General testing unstable

[Makarius]

Here are some hints on using more recent versions of Proof General 
sucessfully (the stable version distributed with Isabelle2008 is still 
ProofGeneral-3.7pre071112):

  * Official 3.7 does not work very well, use pre-3.7.1 from 
    http://proofgeneral.inf.ed.ac.uk/devel instead.

  * Note that recent PG versions also work with native Carbon Emacs on Mac 
    OS X, with regular Unicode support instead of strange X11 fonts.

  * The infamous sledgehammer message problem can be worked around by 
changing a single line in generic/proof-shell.el:

diff -r9.2 proof-shell.el
1391c1391
<             (- (point) proof-shell-eager-annotation-start-length)
---
>             (- (point) (1+ proof-shell-eager-annotation-start-length))


  Here is a context diff of the same change:

*** generic/proof-shell.el      6 Feb 2008 23:04:33 -0000       9.2
--- generic/proof-shell.el      16 Jun 2008 12:49:43 -0000
***************
*** 1388,1394 ****
          ;; should never be any such messages!
          ;; (max
          ;;  (marker-position proof-marker)
!             (- (point) proof-shell-eager-annotation-start-length)
          (1- (process-mark (get-buffer-process (current-buffer))))))
        ;; Otherwise, the search for the ending annotation was
        ;; unsuccessful, so we set the scanner marker to the start of
--- 1388,1394 ----
          ;; should never be any such messages!
          ;; (max
          ;;  (marker-position proof-marker)
!             (- (point) (1+ proof-shell-eager-annotation-start-length))
          (1- (process-mark (get-buffer-process (current-buffer))))))
        ;; Otherwise, the search for the ending annotation was
        ;; unsuccessful, so we set the scanner marker to the start of


As usual, any problem reports should be fed into 
http://proofgeneral.inf.ed.ac.uk/trac/

Recently some Coq power users have been roaring ahead in tweaking Proof 
General, so we should lag behind.


	Makarius