From 78a79e474a3b647e4a32af760ceab3559f1abb5d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 11 Oct 2010 18:07:55 +0000
Subject: proof-debug: fiddle with warning levels to make *PG Debug* buffer
 appear, set it in help mode.

---
 generic/proof-utils.el | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

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

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 6bf9e53e..eb170e23 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -337,13 +337,18 @@ No effect if buffer is dead."
 
 ;;;###autoload
 (defun proof-debug (msg &rest args)
-  "Issue the debugging message (format MSG ARGS) in the response buffer, display it.
+  "Issue the debugging message (format MSG ARGS) in the *PG Debug* buffer.
 If proof-general-debug is nil, do nothing."
-  (if proof-general-debug
-      (let ((formatted (apply 'format msg args)))
+  (when proof-general-debug
+    (with-current-buffer (get-buffer-create "*PG Debug*")
+      (help-mode)
+      (let ((formatted (apply 'format msg args))
+	    (log-warning-minimum-level :debug)
+	    (warning-minimum-level :debug)
+	    (buffer-read-only nil))
 	(display-warning 'proof-general
-			 formatted 'debug
-			 "*PG Debug*"))))
+			 formatted :debug
+			 "*PG Debug*")))))
 
 ;; Utility used in the "Buffers" menu, and throughout
 (defun proof-switch-to-buffer (buf &optional noselect)
-- 
cgit v1.2.3