Disable undo history for efficiency; improve kill buffer hook.

1 files changed, 10 insertions, 8 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 35f3d0f3..fdb5413d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -436,14 +436,13 @@ exited by hand (or exits by itself)."
       ;; Run hooks
       (run-hooks 'proof-shell-kill-function-hooks)
       ;; Kill buffers associated with shell buffer
-      (dolist
-	  (buf '(proof-goals-buffer 
-		 proof-response-buffer 
-		 proof-trace-buffer))
-	(if (buffer-live-p (eval buf))
-	    (progn 
-	      (kill-buffer (eval buf))
-	      (set buf nil))))
+      (let ((proof-shell-buffer nil)) ;; fool kill buffer hooks
+ 	(dolist (buf '(proof-goals-buffer proof-response-buffer 
+					  proof-trace-buffer))
+ 	  (if (buffer-live-p (eval buf))
+ 	      (progn 
+ 		(kill-buffer (eval buf))
+ 		(set buf nil)))))
       (message "%s exited." bufname))))
 
 (defun proof-shell-clear-state ()
@@ -1694,6 +1693,9 @@ usual, unless NOERROR is non-nil."
 
   (make-local-variable 'proof-shell-insert-hook)
 
+  ;; Efficiency: don't keep undo history
+  (buffer-disable-undo)
+
   ;; comint customisation. comint-prompt-regexp is used by
   ;; comint-get-old-input, comint-skip-prompt, comint-bol, backward
   ;; matching input, etc.