diff options
| -rw-r--r-- | generic/proof-shell.el | 11 | ||||
| -rw-r--r-- | generic/proof.el | 5 |
2 files changed, 9 insertions, 7 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index c0d6dcdd..8a1e2ba5 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -821,9 +821,9 @@ See the documentation for `proof-shell-delayed-output' for further details." ;; Erase the response buffer if need be, and indicate that ;; it is to be erased again before the next message. (proof-shell-maybe-erase-response t nil) - (let ((pos (point))) - (insert str) - (proof-x-symbol-decode-region pos (point))) + (setq pos (point)) + (insert str) + (proof-x-symbol-decode-region pos (point)) (proof-display-and-keep-buffer proof-response-buffer))) ;; ;; 2. Text to be inserted in goals buffer @@ -874,8 +874,8 @@ Then we call `proof-shell-handle-error-hook'. " (save-excursion ;current-buffer (set-buffer proof-goals-buffer) (erase-buffer) - (insert (proof-shell-strip-special-annotations - (cdr proof-shell-delayed-output))) + (insert (cdr proof-shell-delayed-output)) + (proof-x-symbol-decode-region (point-min) (point-max)) (proof-display-and-keep-buffer proof-goals-buffer))) ;; This prevents problems if the user types in the @@ -1509,6 +1509,7 @@ however, are always processed; hence their name)." (progn (backward-char (- (match-end 0) (match-beginning 0))) (setq string (buffer-substring startpos (point))) + (proof-x-symbol-decode-region startpos (point)) (goto-char (point-max)) (proof-shell-filter-process-output string))))))))) diff --git a/generic/proof.el b/generic/proof.el index 7625dae3..ff25563e 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -160,10 +160,11 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding (newline) (setq start (point)) (insert str) - (setq end (point)) + (proof-x-symbol-decode-region start (point)) + (setq end (point-max)) (save-excursion (font-lock-set-defaults) ;required for FSF Emacs 20.2 - (font-lock-fontify-region start end) +;DvO (font-lock-fontify-region start end) (if face (font-lock-append-text-property start end 'face face))) (buffer-substring start end)))) |