From 8ab8b91b1b44ad0a5d265ecded32276723671f91 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 10 Sep 2009 23:45:38 +0000
Subject: Move stripping and minibuffer-message function here

---
 generic/proof-utils.el | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

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

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 7347ab58..a37bcf85 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -943,6 +943,25 @@ it calls `proof-looking-at-syntactic-context'."
     (proof-looking-at-syntactic-context-default)))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Stripping output and message 
+;;
+
+(defsubst proof-shell-strip-output-markup (string &optional push)
+  "Strip output markup from STRING.
+Convenience function to call function `proof-shell-strip-output-markup'.
+Optional argument PUSH is ignored."
+  (funcall proof-shell-strip-output-markup string))
+
+(defun proof-minibuffer-message (str)
+  "Output STR in minibuffer."
+  (if proof-minibuffer-messages
+      (message "%s" ;; to escape format characters
+	       (concat "[" proof-assistant "] "
+		       ;; TODO: rather than stripping, could try fontifying
+		       (proof-shell-strip-output-markup str)))))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-- 
cgit v1.2.3