From 00c337af2ea574baf01a26581b80aa1fd955e2f0 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Fri, 30 Oct 1998 16:34:38 +0000
Subject: implemented new buffer model. The goals buffer is now exclusively
 reserved for goals.

---
 generic/proof-script.el | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index fa09ede9..624a468e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -272,10 +272,7 @@ to allow other files loaded by proof assistants to be marked read-only."
 (defun proof-warning (str)
   "Issue the warning STR."
     (proof-response-buffer-display str 'proof-warning-face)
-    (display-buffer proof-response-buffer)
-    (set-window-dedicated-p
-     (get-buffer-window proof-response-buffer) 'dedicated))
-
+    (proof-display-and-keep-buffer proof-response-buffer))
 
 (defun proof-register-possibly-new-processed-file (file)
   "Register a possibly new FILE as having been processed by the prover."
-- 
cgit v1.2.3