aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-useropts.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2012-08-16 15:01:05 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2012-08-16 15:01:05 +0000
commitd1dbb1bb03f777f744774b353b13b3cf2d11bf5f (patch)
tree4544c59fbd97b3d276456867d1b50173276082af /generic/proof-useropts.el
parent3ace4262f67f259cba60338db8718d134c2c237c (diff)
Add option proof-layout-windows-on-visit-file, addressing Trac #444
Diffstat (limited to 'generic/proof-useropts.el')
-rw-r--r--generic/proof-useropts.el11
1 files changed, 10 insertions, 1 deletions
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