Hi,
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 ...
Bye,
Hendrik
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
(proof-deactivate-scripting))
(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
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
