Move stripping and minibuffer-message function here

1 files changed, 19 insertions, 0 deletions

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)))))
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;