[nongnu] elpa/proof-general 3c9bed7061 1/8: Add an option to stop proof-shell-kill-function from killing buffers.

[ELPA Syncer]

branch: elpa/proof-general
commit 3c9bed7061b420070a068502eefe592685fea800
Author: Calvin Beck <hobbes@ualberta.ca>
Commit: Calvin Beck <hobbes@ualberta.ca>

    Add an option to stop proof-shell-kill-function from killing buffers.
---
 generic/proof-shell.el    | 33 +++++++++++++++++++--------------
 generic/proof-useropts.el | 11 +++++++++++
 2 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3407a0fbd8..3e6d5ac03f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -494,6 +494,22 @@ process command."
 (defvar proof-shell-kill-function-hooks nil
   "Functions run from `proof-shell-kill-function'.")
 
+(defun proof-shell-kill-function-kill-associated-buffers ()
+  "Kill the goal, response, and trace buffers, as well as frames if necessary."
+  ;; Remove auxiliary windows, trying to stop proliferation of
+  ;; frames (NB: loses if user has switched buffer in special frame)
+  (if (and proof-multiple-frames-enable
+          proof-shell-fiddle-frames)
+      (proof-delete-all-associated-windows))
+
+  (let ((proof-shell-buffer nil)) ;; fool kill buffer hooks
+    (dolist (buf '(proof-goals-buffer proof-response-buffer
+                                     proof-trace-buffer))
+      (when (buffer-live-p (symbol-value buf))
+        (delete-windows-on (symbol-value buf))
+        (kill-buffer (symbol-value buf))
+        (set buf nil)))))
+
 (defun proof-shell-kill-function ()
   "Function run when a proof-shell buffer is killed.
 Try to shut down the proof process nicely and clear locked
@@ -544,20 +560,9 @@ shell buffer, called by `proof-shell-bail-out' if process 
exits."
     (proof-shell-clear-state)
     (run-hooks 'proof-shell-kill-function-hooks)
 
-    ;; Remove auxiliary windows, trying to stop proliferation of
-    ;; frames (NB: loses if user has switched buffer in special frame)
-    (if (and proof-multiple-frames-enable
-            proof-shell-fiddle-frames)
-       (proof-delete-all-associated-windows))
-
-    ;; Kill associated buffer
-    (let ((proof-shell-buffer nil)) ;; fool kill buffer hooks
-      (dolist (buf '(proof-goals-buffer proof-response-buffer
-                                       proof-trace-buffer))
-       (when (buffer-live-p (symbol-value buf))
-         (delete-windows-on (symbol-value buf))
-         (kill-buffer (symbol-value buf))
-         (set buf nil))))
+    (when proof-shell-kill-function-also-kills-associated-buffers
+      (proof-shell-kill-function-kill-associated-buffers))
+
     (setq proof-shell-exit-in-progress nil)
     (message "%s exited." bufname)))
 
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 9edeec437a..7df22040e8 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -230,6 +230,17 @@ selected frame will be automatically deleted."
   :type 'boolean
   :group 'proof-user-options)
 
+(defcustom proof-shell-kill-function-also-kills-associated-buffers t
+  "*If non-nil, when `proof-shell-kill-function' is called, clean up buffers.
+For example, `proof-shell-kill-function' is called when buffers
+are retracted when switching between proof script files. It may
+make sense to set this to `nil' when
+`proof-multiple-frames-enable' is set to prevent proof general
+from killing frames that you want to be managed by a window
+manager instead of within emacs."
+  :type 'boolean
+  :group 'proof-user-options)
+
 (defcustom proof-shrink-windows-tofit nil
   "*If non-nil, automatically shrink output windows to fit contents.
 In single-frame mode, this option will reduce the size of the