Fixing #25.

proof-script-buffer was not set before calling proof-shell-ready-prover.

2 files changed, 5 insertions, 8 deletions

diff --git a/coq/coq.el b/coq/coq.el
index c06a7744..e83c1dbc 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2452,12 +2452,8 @@ number of hypothesis displayed, without hiding the goal"
 (defun is-not-split-vertic (selected-window)
   (<= (- (frame-height) (window-height)) 2))
 
-;; three window mode needs to be called when starting the script
-(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
-
-;; three window mode needs to be called when starting the script
-(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
-
+;; bug fixed in generic ocde, useless now:
+;(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
 
 ;; *Experimental* auto shrink response buffer in three windows mode. Things get
 ;; a bit messed up if the response buffer is not at the right place (below
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e65d2fc9..3a24595e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1240,11 +1240,12 @@ activation is considered to have failed and an error is given."
       (assert (null proof-script-buffer)
 	      "Bug in proof-activate-scripting: deactivate failed.")
 
+      ;; Set the active scripting buffer, and initialise regions
+      (setq proof-script-buffer (current-buffer))
+
       ;; Fire up the prover (or check it's going the right way).
       (proof-shell-ready-prover queuemode)
 
-      ;; Set the active scripting buffer, and initialise regions
-      (setq proof-script-buffer (current-buffer))
       (if (proof-locked-region-empty-p) ; leave alone if non-empty
 	  (proof-init-segmentation))