diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2012-08-16 15:01:05 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2012-08-16 15:01:05 +0000 |
commit | d1dbb1bb03f777f744774b353b13b3cf2d11bf5f (patch) | |
tree | 4544c59fbd97b3d276456867d1b50173276082af /generic | |
parent | 3ace4262f67f259cba60338db8718d134c2c237c (diff) |
Add option proof-layout-windows-on-visit-file, addressing Trac #444
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-response.el | 13 | ||||
-rw-r--r-- | generic/proof-menu.el | 6 | ||||
-rw-r--r-- | generic/proof-script.el | 11 | ||||
-rw-r--r-- | generic/proof-shell.el | 31 | ||||
-rw-r--r-- | generic/proof-useropts.el | 11 |
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 |