for coq there is currently a problem when you switch the active
scripting buffer: The first assert command in the new scripting
buffer does not assert anything. 

This happens, because coq mode kills the proof assistant in the
deactivation hooks and proof-activate-scripting runs those hooks
_after_ proof-shell-ready-prover.

Below I append a patch that fixes this problem for me. Please
review this patch, because I have not much understanding of what
I am changing...

There are two points about the patch:

- I first experimented with calling proof-shell-ready-prover
  after the big unless-form in proof-activate-scripting. This was
  running fine for me, but then I figured it would be better if
  the proof assistant is restarted before the activation hooks
  run. Now proof-shell-ready-prover is called in the middle of
  the unless-form (which has been split into two halves).

- When I first tested this patch back in January, it was not
  sufficient. Back then the patch ensured that the proof
  assistant was running after proof-activate-scripting, but the
  first assert in the new scripting buffer was nevertheless lost
  (because, IMO, proof-shell-exit killed all spans). 

  However, I cannot reproduce this problem any more, not even
  with old Proof General versions from January. The patch below
  is working correctly for me ...



Index: generic/proof-script.el
RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-script.el,v
retrieving revision 11.8
diff -u -r11.8 proof-script.el
--- generic/proof-script.el     31 Jan 2011 10:35:55 -0000      11.8
+++ generic/proof-script.el     14 Feb 2011 12:05:54 -0000
@@ -1196,8 +1196,14 @@
   (unless (eq proof-buffer-type 'script)
     (error "Must be running in a script buffer!"))
-  (proof-shell-ready-prover queuemode) ; fire up/check mode
+  ;; Check whether we have a new or changed proof-script-buffer. If
+  ;; this is the case, a lot of things must be done. We split all
+  ;; these things into two halves. The first half follows immediately:
+  ;; it shuts down the old proof-script-buffer and retracts some
+  ;; files. The second half initializes the new proof-script-buffer.
+  ;; Because the first half might kill the prover (which is actually
+  ;; the case for coq), we make sure the proof shell is ready before
+  ;; we start the second half.
   (unless (equal (current-buffer) proof-script-buffer)
     ;; TODO: narrow the scope of this save-excursion.
@@ -1228,10 +1234,18 @@
       (if proof-script-buffer
       (assert (null proof-script-buffer)
-             "Bug in proof-activate-scripting: deactivate failed.")
+             "Bug in proof-activate-scripting: deactivate failed.")))
-      ;; Set the active scripting buffer, and initialise regions
+  (proof-shell-ready-prover queuemode) ; fire up/check mode
+  ;; It now follows the second half of things to do if we have a new
+  ;; or changed proof-script-buffer.
+  (unless (equal (current-buffer) proof-script-buffer)
+    ;; TODO: (copied from above) narrow the scope of this save-excursion.
+    ;; Where is it needed?  Maybe hook functions.
+    (save-excursion
+      ;; Set the active scripting buffer, and initialise regions
       (setq proof-script-buffer (current-buffer))
       (if (proof-locked-region-empty-p)
          ;; Clear locked regions, unless buffer is "full".
ProofGeneral-devel mailing list

Reply via email to