diff options
| author | David Aspinall | 2008-01-15 18:34:35 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-15 18:34:35 +0000 |
| commit | 776627a70a4403313505f6ac71538fb700693fa6 (patch) | |
| tree | 3d2e2d79481d9fcba6c06690fc3e3a8388b3ddb4 /generic/proof-shell.el | |
| parent | eba528f89f69805fdf3b0f190065353867536741 (diff) | |
Before calling pg-response-display-with-face, strip eager annotation but not specials.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 63c42a88..8f9b74c9 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1370,9 +1370,7 @@ MESSAGE should be a string annotated with (substring stripped 0 (or (string-match "\n" stripped) (min (length stripped) 75)))) (pg-response-display-with-face - (if pg-use-specials-for-fontify - message - stripped) + (proof-shell-strip-eager-annotations message) 'proof-eager-annotation-face))))) (defun proof-shell-strip-eager-annotations (string) |