diff options
| -rw-r--r-- | generic/proof-utils.el | 19 |
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))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |