Added proof-auto-delete-windows user option.

2 files changed, 14 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1207163d..0af8af7e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -132,6 +132,14 @@ 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
+  "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.")
 
 ;;
 ;; Faces.
diff --git a/generic/proof.el b/generic/proof.el
index 4fad6308..849f6f76 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -58,6 +58,9 @@
 (autoload 'proof-shell-available-p "proof-shell"
   "Returns non-nil if there is a proof shell active and available.")
 
+(autoload 'proof-shell-invisible-command "proof-shell"
+  "Send CMD to the proof process without revealing it to the user.")
+
 ;;;
 ;;; Global variables
 ;;;
@@ -168,11 +171,12 @@ Also ensures that point is visible."
 		 (recenter -1)))))))
 
 (defun proof-clean-buffer (buffer)
-  "Erase buffer and hide from display."
+  "Erase buffer and hide from display if proof-auto-delete-windows set"
   (save-excursion
     (set-buffer buffer)
     (erase-buffer))
-  (delete-windows-on buffer))
+  (if proof-auto-delete-windows
+      (delete-windows-on buffer)))
 
 (provide 'proof)
 ;; proof.el ends here