Fixing a bug happening in coq when three win mode on and scripting

starts on a buffer. The response buffer was hiding the scripting
buffer.

NOTE: this is not a bug correction. The bug is still there but
proof-layout-windows is called to work it around.

1 files changed, 8 insertions, 7 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 252d8458..ce43bef2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -880,12 +880,11 @@ flag Printing All set."
   (interactive "P")
   (if (proof-in-locked-region-p)
       (let ((s (coq-get-response-string-at)))
-        (save-excursion 
-          (set-buffer proof-response-buffer)
-          (let ((inhibit-read-only 'titi))
-            (pg-response-display s)
-            (proof-display-and-keep-buffer proof-response-buffer)
-            (coq-optimise-resp-windows))))
+        (set-buffer proof-response-buffer)
+        (let ((inhibit-read-only 'titi))
+          (pg-response-display s)
+          (proof-display-and-keep-buffer proof-response-buffer)
+          (coq-optimise-resp-windows)))
     (if withprintingall
         (coq-ask-do-show-all "Show goal number" "Show" t)
       (coq-ask-do "Show goal number" "Show" t))))
@@ -913,7 +912,7 @@ flag Printing All set."
   "Compiles current buffer."
   (interactive)
   (let* ((n (buffer-name))
-	 (l (string-match ".v" n)))
+         (l (string-match ".v" n)))
     (compile (concat "make " (substring n 0 l) ".vo"))))
 
 
@@ -2632,6 +2631,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))))
 
 ;; *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