From 278e065741e2959258b862407e53fe9d4a9ef418 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Jan 2002 16:35:43 +0000
Subject: Also bury trace buffer

---
 generic/proof-script.el | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7e10dcbc..fc2e618b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2277,13 +2277,12 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
       (if (eq (current-buffer) proof-script-buffer)
 	  (proof-deactivate-scripting 'retract))
     (proof-restart-buffers (list (current-buffer)))
-    ;; Hide away goals and response: this is a hack because otherwise
-    ;; we can lead the user to frustration with the dedicated windows
-    ;; nonsense.
-    (if (buffer-live-p proof-goals-buffer) 
-	(bury-buffer proof-goals-buffer))
-    (if (buffer-live-p proof-response-buffer)
-	(bury-buffer proof-response-buffer))))
+    ;; Hide away goals, response, and tracing.  This is a hack because
+    ;; otherwise we can lead the user to frustration with the
+    ;; dedicated windows nonsense.
+    (proof-map-buffers 
+     (list proof-goals-buffer proof-response-buffer proof-trace-buffer)
+     (bury-buffer (current-buffer)))))
 
 
 ;; Notes about how to deal with killing/reverting/renaming buffers:
-- 
cgit v1.2.3