diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 8 | ||||
| -rw-r--r-- | generic/proof-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-script.el | 8 | ||||
| -rw-r--r-- | generic/proof.el | 4 |
4 files changed, 11 insertions, 11 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index eff09dd7..51f4fb7c 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1873,10 +1873,10 @@ The default value is @code{nil}. Sometimes during script management, there is no response from the proof assistant to some command. In this case you might like the empty response window to be hidden so you have more room to see the proof -script. The setting @code{proof-auto-delete-windows} helps you do this. +script. The setting @code{proof-delete-empty-windows} helps you do this. -@c TEXI DOCSTRING MAGIC: proof-auto-delete-windows -@defopt proof-auto-delete-windows +@c TEXI DOCSTRING MAGIC: proof-delete-empty-windows +@defopt proof-delete-empty-windows If non-nil, automatically remove windows when they are cleaned.@* For example, at the end of a proof the goals buffer window will be cleared; if this flag is set it will automatically be removed. @@ -1904,7 +1904,7 @@ the goals and response buffers, by altering the Emacs variable The default value is @code{nil}. @end defopt -Multiple frames work best when @code{proof-auto-delete-windows} is off +Multiple frames work best when @code{proof-delete-empty-windows} is off and @code{proof-dont-switch-windows} is on. diff --git a/generic/proof-config.el b/generic/proof-config.el index 36bac31f..88badbc8 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -184,7 +184,7 @@ the goals and response buffers, by altering the Emacs variable :set 'proof-set-bool :group 'proof-user-options) -(defcustom proof-auto-delete-windows +(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 diff --git a/generic/proof-script.el b/generic/proof-script.el index ccfde84c..89f4129c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2239,8 +2239,8 @@ This is intended as a value for proof-activate-scripting-hook" ;; Make the togglers used in options menu below (fset 'proof-dont-switch-windows-toggle (proof-customize-toggle proof-dont-switch-windows)) -(fset 'proof-auto-delete-windows-toggle - (proof-customize-toggle proof-auto-delete-windows)) +(fset 'proof-delete-empty-windows-toggle + (proof-customize-toggle proof-delete-empty-windows)) (fset 'proof-multiple-frames-toggle (proof-customize-toggle proof-multiple-frames-enable)) (fset 'proof-output-fontify-toggle @@ -2254,10 +2254,10 @@ This is intended as a value for proof-activate-scripting-hook" :active t :style toggle :selected proof-dont-switch-windows] - ["Delete empty windows" proof-auto-delete-windows-toggle + ["Delete empty windows" proof-delete-empty-windows-toggle :active t :style toggle - :selected proof-auto-delete-windows] + :selected proof-delete-empty-windows] ["Multiple frames" proof-multiple-frames-toggle :active t :style toggle diff --git a/generic/proof.el b/generic/proof.el index f23c21dc..4fff00f9 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -417,13 +417,13 @@ Ensure that point is visible in window." (recenter -1))))))) (defun proof-clean-buffer (buffer) - "Erase buffer and hide from display if proof-auto-delete-windows set. + "Erase buffer and hide from display if proof-delete-empty-windows set. Auto deletion only affects selected frame. (We assume that the selected frame is the one showing the script buffer.)" (with-current-buffer buffer ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(. (erase-buffer) - (if proof-auto-delete-windows + (if proof-delete-empty-windows (delete-windows-on buffer t)))) (defun proof-message (&rest args) |