diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-26 17:39:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-26 17:39:25 +0000 |
| commit | add6299da8e4fcbb2efa16d75b9126a536cdfca5 (patch) | |
| tree | 0cd39795c3f958d6dc24017e13e4c08cdab061aa | |
| parent | 5301fd94b22fa5e59dfcccc19e89e2f3faccd21e (diff) | |
Try to prevent associated buffers being killed off by user.
| -rw-r--r-- | generic/pg-goals.el | 3 | ||||
| -rw-r--r-- | generic/pg-response.el | 2 | ||||
| -rw-r--r-- | generic/proof-utils.el | 18 |
3 files changed, 22 insertions, 1 deletions
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 @@ -244,6 +244,24 @@ Restrict to BUFLIST if it's set." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;; 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 (defun proof-define-keys (map kbl) |