From add6299da8e4fcbb2efa16d75b9126a536cdfca5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 26 Aug 2002 17:39:25 +0000
Subject: Try to prevent associated buffers being killed off by user.

---
 generic/pg-goals.el    |  3 ++-
 generic/pg-response.el |  2 ++
 generic/proof-utils.el | 18 ++++++++++++++++++
 3 files changed, 22 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 8d854ce3..2e98fd73 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -26,8 +26,9 @@
   "Mode for goals display.  
 May enable proof-by-pointing or similar features.
 \\{proof-goals-mode-map}"
-  ;; defined-derived-mode proof-goals-mode initialises proof-goals-mode-map
   (setq proof-buffer-type 'goals)
+  (make-local-hook 'kill-buffer-hook)
+  (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
   (easy-menu-add proof-assistant-menu proof-goals-mode-map)
   (proof-toolbar-setup)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 2d2a46ba..df3627d1 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -22,6 +22,8 @@
   "PGResp" "Responses from Proof Assistant"
   (setq proof-buffer-type 'response)
   (define-key proof-response-mode-map [q] 'bury-buffer)
+  (make-local-hook 'kill-buffer-hook)
+  (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-response-mode-menu proof-response-mode-map)
   (easy-menu-add proof-assistant-menu proof-response-mode-map)
   (proof-toolbar-setup)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 18ca1db8..e060d5af 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -242,6 +242,24 @@ Restrict to BUFLIST if it's set."
       (if (with-current-buffer buf (eq mode major-mode))
 	  (setq bufs-got (cons buf bufs-got))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Associated buffers
+;;
+
+(defun pg-save-from-death ()
+  "Prevent this associated buffer from being killed.
+A hook function for `kill-buffer-hook'.
+This is a fairly crude and not-entirely-robust way to prevent the 
+user accidently killing an associated buffer."
+  (if (and (proof-shell-live-buffer) proof-buffer-type)
+      (progn
+	(let ((bufname (buffer-name)))
+	  (bury-buffer)
+	  (message 
+	   "Warning: buffer %s not killed; still associated with prover process."
+	   bufname)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Key functions
-- 
cgit v1.2.3