aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--generic/proof-config.el12
-rw-r--r--generic/proof.el10
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