diff options
| -rw-r--r-- | generic/proof-config.el | 12 | ||||
| -rw-r--r-- | generic/proof.el | 10 |
2 files changed, 12 insertions, 10 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index b2841667..e2dedb1d 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -132,14 +132,16 @@ The protocol used should be configured so that no user interaction :type 'string :group 'proof-general) -(defcustom proof-auto-delete-windows nil - ;; da: I've set default to nil for principle of least surprise +(defcustom proof-auto-delete-windows t "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. -If you use several frames to display the Proof General buffers, -you may want to set this variable to 'nil' to avoid frames being -deleted automatically.") +If you want to fix the sizes of your windows you may want to set this +variable to 'nil' to avoid windows being deleted automatically. +If you use multiple frames, only the windows in the currently +selected frame will be affected." + :type 'boolean + :group 'proof-general) ;; ;; Faces. diff --git a/generic/proof.el b/generic/proof.el index db56e40f..09458c13 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -181,12 +181,12 @@ Also ensures that point is visible." (recenter -1))))))) (defun proof-clean-buffer (buffer) - "Erase buffer and hide from display if proof-auto-delete-windows set" - (save-excursion - (set-buffer buffer) - (erase-buffer)) + "Erase buffer and hide from display if proof-auto-delete-windows set. +Auto deletion only affects selected frame. (We assume that the selected +frame is the one showing the script buffer.)" + (erase-buffer buffer) (if proof-auto-delete-windows - (delete-windows-on buffer))) + (delete-windows-on buffer t))) (provide 'proof) ;; proof.el ends here |
