diff options
| author | David Aspinall | 2009-09-10 23:45:38 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-10 23:45:38 +0000 |
| commit | 8ab8b91b1b44ad0a5d265ecded32276723671f91 (patch) | |
| tree | 1f4fe6611a352661bc4dae2657a2ec8ec6ebd19d | |
| parent | a1117eb133936608ad50ec713e1812dece586a6b (diff) | |
Move stripping and minibuffer-message function here
| -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))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |