Add option proof-layout-windows-on-visit-file, addressing Trac #444

5 files changed, 47 insertions, 25 deletions

diff --git a/generic/pg-response.el b/generic/pg-response.el
index 9edead81..c95d8cce 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -110,7 +110,7 @@ Internal variable, setting this will have no effect!")
   (proof-layout-windows))
 
 (defun proof-select-three-b (b1 b2 b3 &optional nohorizontalsplit)
-  "Select three buffers. Put them into three windows, selecting the last one."
+  "Put the given three buffers into three windows."
   (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
   (delete-other-windows)
   (if nohorizontalsplit
@@ -127,13 +127,12 @@ Internal variable, setting this will have no effect!")
 (defun proof-display-three-b (&optional nohorizontalsplit)
   "Layout three buffers in a single frame.  Only do this if buffers exist."
   (interactive)
-  (when (and proof-script-buffer
-	     (buffer-live-p proof-goals-buffer)
+  (when (and (buffer-live-p proof-goals-buffer)
 	     (buffer-live-p proof-response-buffer))
-    (proof-select-three-b
-     proof-script-buffer proof-goals-buffer proof-response-buffer
-     nohorizontalsplit)))
-
+    (save-excursion
+      (proof-select-three-b
+       proof-script-buffer proof-goals-buffer proof-response-buffer
+       nohorizontalsplit))))
 
 (defvar pg-frame-configuration nil
   "Variable storing last used frame configuration.")
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 472f2f9e..a88c3e08 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -285,6 +285,8 @@ without adjusting window layout."
 (proof-deftoggle proof-delete-empty-windows)
 (proof-deftoggle proof-shrink-windows-tofit)
 (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
+(proof-deftoggle proof-layout-windows-on-visit-file 
+		 proof-layout-windows-eagerly-toggle)
 (proof-deftoggle proof-three-window-enable proof-three-window-toggle)
 (proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle)
 (proof-deftoggle proof-disappearing-proofs)
@@ -397,6 +399,10 @@ without adjusting window layout."
       ;; We use non-Emacs terminology "Windows" in this menu to help
       ;; non-Emacs users.  Cf. Gnome usability studies: menus saying
       ;; "Web Browser" more useful to novices than menus saying "Mozilla"!!
+      ["Layout Eagerly" proof-layout-windows-eagerly-toggle
+       :style toggle
+       :selected proof-layout-windows-on-visit-file
+       :help "Display prover output windows when script file is opened."]
       ["Multiple Windows" proof-multiple-frames-toggle
        :active (and window-system t)
        :style toggle
diff --git a/generic/proof-script.el b/generic/proof-script.el
index d1c469a4..abbfefb3 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -29,6 +29,8 @@
 
 (declare-function proof-shell-strip-output-markup "proof-shell"
 		  (string &optional push))
+(declare-function proof-shell-make-associated-buffers "proof-shell" ())
+(declare-function proof-layout-windows "pg-response" (&rest args))
 (declare-function pg-response-warning "pg-response" (&rest args))
 (declare-function proof-segment-up-to "proof-script")
 (declare-function proof-autosend-enable "pg-user")
@@ -2586,10 +2588,15 @@ finish setup which depends on specific proof assistant configuration."
 	     (cons (pg-invisible-prop p) t)))
 	  pg-all-idioms)
 
-  ;; Finally, make sure the user has been welcomed!
-  ;; [NB: this doesn't work well, can get zapped by loading messages]
+  ;; If we're excited to get going straightaway, make and layout windows
+  (when proof-layout-windows-on-visit-file
+      (proof-shell-make-associated-buffers)
+      (proof-layout-windows))
+
+  ;; Make sure the user has been welcomed!
   (proof-splash-message))
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Subroutines of proof-config-done
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index edd3d510..f64b110e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -236,6 +236,21 @@ If QUEUEMODE is supplied, set the lock to that value."
     ;; Otherwise, chars 128-255 get remapped higher, breaking regexps
     (toggle-enable-multibyte-characters -1)))
 
+(defun proof-shell-make-associated-buffers ()
+  "Create the associated buffers and set buffer variables holding them."
+  (let ((goals	"*goals*")
+	(resp	"*response*")
+	(trace	"*trace*")
+	(thms	"*thms*"))
+    (setq proof-goals-buffer    (get-buffer-create goals))
+    (setq proof-response-buffer (get-buffer-create resp))
+    (if proof-shell-trace-output-regexp
+	(setq proof-trace-buffer (get-buffer-create trace)))
+    (if proof-shell-thms-output-regexp
+	(setq proof-thms-buffer (get-buffer-create thms)))
+    ;; Set the special-display-regexps now we have the buffer names
+    (setq pg-response-special-display-regexp
+	  (proof-regexp-alt goals resp trace thms))))
 
 (defun proof-shell-start ()
   "Initialise a shell-like buffer for a proof assistant.
@@ -345,22 +360,8 @@ process command."
 	  ;; Give error now if shell buffer isn't live (process exited)
 	  (setq proof-shell-buffer nil)
 	  (error "Starting process: %s..failed" prog-command-line)))
-
-      ;; Create the associated buffers and set buffer variables
       
-      (let ((goals	"*goals*")
-	    (resp	"*response*")
-	    (trace	"*trace*")
-	    (thms	"*thms*"))
-	(setq proof-goals-buffer    (get-buffer-create goals))
-	(setq proof-response-buffer (get-buffer-create resp))
-	(if proof-shell-trace-output-regexp
-	    (setq proof-trace-buffer (get-buffer-create trace)))
-	(if proof-shell-thms-output-regexp
-	    (setq proof-thms-buffer (get-buffer-create thms)))
-	;; Set the special-display-regexps now we have the buffer names
-	(setq pg-response-special-display-regexp
-	      (proof-regexp-alt goals resp trace thms)))
+      (proof-shell-make-associated-buffers)
 
       (with-current-buffer proof-shell-buffer
 
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 0a7d8bfe..21fbd321 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -139,7 +139,7 @@ you a reprimand!)."
   :set   'proof-set-value
   :group 'proof-user-options)
 
-(defcustom proof-three-window-enable nil
+(defcustom proof-three-window-enable t
   "*Whether response and goals buffers have dedicated windows.
 If non-nil, Emacs windows displaying messages from the prover will not
 be switchable to display other windows.
@@ -167,6 +167,15 @@ the goals and response buffers, by altering the Emacs variable
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defcustom proof-layout-windows-on-visit-file t
+  "*Whether to eagerly create auxiliary buffers and display windows.
+If non-nil, the output buffers are created and (re-)displayed as soon
+as a proof script file is visited.  Otherwise, the buffers are created
+and displayed lazily.  See `proof-layout-windows'."
+  :type 'boolean
+  :set 'proof-set-value
+  :group 'proof-user-options)
+
 (defcustom proof-delete-empty-windows nil
   "*If non-nil, automatically remove windows when they are cleaned.
 For example, at the end of a proof the goals buffer window will