diff options
| author | David Aspinall | 1998-10-26 14:05:18 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-26 14:05:18 +0000 |
| commit | ad5f150b0eb16f90fa034eb3cfd8378a38a4506d (patch) | |
| tree | 96b7fee0a40004334af7a2b15eb26594c3e92c52 | |
| parent | d858652f7fcd6f3a3da1b032ef879f508cfa5f49 (diff) | |
Moved proof-message to proof shell, renamed to proof-shell-message.
Removed redundant variables in proof-shell-popup-eager-annotation.
| -rw-r--r-- | generic/proof-shell.el | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 45220366..6630db9a 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -735,6 +735,10 @@ at the end of locked region (after inserting a newline and indenting)." ;; eager annotations are one line long, and we get input a line at a ;; time. If we go over to piped communication, it will break. +(defun proof-shell-message (str) + "Output STR in minibuffer." + (message (concat "[" proof-assistant "] " str))) + ;; FIXME: highlight eager annotation-end : fix proof-shell-handle-output ;; to highlight whole string. (defun proof-shell-popup-eager-annotation () @@ -747,8 +751,7 @@ arrive." proof-shell-eager-annotation-start proof-shell-eager-annotation-end 'proof-eager-annotation-face)) - file module) - (proof-message str))) + (proof-shell-message str)))) (defun proof-response-buffer-display (str face) "Display STR with FACE in response buffer." @@ -794,7 +797,7 @@ arrive." (set-difference current-included proof-included-files-list)))))) (t - (proof-message message) + (proof-shell-message message) (proof-response-buffer-display message 'proof-eager-annotation-face)))) |