From 9d11b325cee534c5a166a135d6c7c97740e00670 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 31 Aug 2012 20:31:13 +0000 Subject: 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. --- coq/coq.el | 15 ++++++++------- 1 file 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 -- cgit v1.2.3