Added new face for debug messages

2 files changed, 36 insertions, 5 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 506fa692..1bae2e5c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -468,7 +468,17 @@ Warning messages can come from proof assistant or from Proof General itself."
      (:background "darkgoldenrod"))
     (t				
      (:italic t)))
-  "*Face for messages from proof assistant."
+  "*Face for important messages from proof assistant."
+  :group 'proof-faces)
+
+(defface proof-debug-message-face
+  '((((type x) (class color) (background light))   
+     (:foreground "Gray65"))
+    (((type x) (class color) (background dark))   
+     (:background "Gray30"))
+    (t				
+     (:italic t)))
+  "*Face for debugging messages from Proof General."
   :group 'proof-faces)
 
 
@@ -1309,8 +1319,16 @@ into tokens for the proof assistant."
 
 (defcustom proof-pre-shell-start-hook nil
   "Hooks run before proof shell is started.
-Suggestion: set this to a function which configures the proof shell
-variables."
+Suggestion: set this to a function which configures just these proof
+shell variables: 
+
+   proof-prog-name
+   proof-mode-for-shell
+   proof-mode-for-response
+   proof-mode-for-pbp
+
+This is the bare minimum needed to get a shell buffer and
+its friends configured in the function proof-shell-start."
   :type '(repeat function)
   :group 'proof-shell)
 
@@ -1537,6 +1555,13 @@ tokens (for example, editing documentation or source code files)."
   :type 'sexp
   :group 'proof-x-symbol)
 
+(defcustom proof-xsym-activate-command nil
+  "Command to activate token input/output for X-Symbol.
+If non-nil, this command is sent to the proof assistant when 
+X-Symbol support is activated."
+  :type 'string
+  :group 'proof-x-symbol)
+
 (defcustom proof-xsym-deactivate-command nil
   "Command to deactivate token input/output for X-Symbol.
 If non-nil, this command is sent to the proof assistant when 
@@ -1551,6 +1576,7 @@ X-Symbol support is deactivated."
 
 
 
+
 
 ;;
 ;; 9. Global constants
diff --git a/generic/proof.el b/generic/proof.el
index 82996cf8..dd18ce2a 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -400,11 +400,16 @@ The warning is coloured with proof-warning-face."
     (proof-response-buffer-display (apply 'concat args) 'proof-warning-face)
     (proof-display-and-keep-buffer proof-response-buffer))
 
-(defmacro proof-debug (&rest args)
+;; could be a macro for efficiency in compiled code
+(defun proof-debug (&rest args)
   "Issue the debugging messages ARGS in the response buffer, display it.
 If proof-show-debug-messages is nil, do nothing."
   (if proof-show-debug-messages
-      `(proof-warning ,@args)))
+      (progn
+	(proof-response-buffer-display (apply 'concat args) 
+				       'proof-debug-message-face)
+	(proof-display-and-keep-buffer proof-response-buffer))))
+