diff options
| -rw-r--r-- | generic/pg-goals.el | 7 | ||||
| -rw-r--r-- | generic/pg-response.el | 3 |
2 files changed, 7 insertions, 3 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 60420b19..e726ecdd 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -127,8 +127,11 @@ and properly fontifies STRING using proof-fontify-region." ;; but keep specials in case also used for subterm markup. (proof-fontify-region (point-min) (point-max) 'keepspecials)) - ;; Markup for PBP-style interaction - (pg-goals-analyse-structure (point-min) (point-max)) + ;; Markup for PBP-style interaction. This currently only works + ;; for special characters 128-255, which is inconsistent with + ;; UTF-8 interaction. + (unless proof-shell-unicode + (pg-goals-analyse-structure (point-min) (point-max))) (unless pg-use-specials-for-fontify ;; provers which use ordinary keywords to fontify output must diff --git a/generic/pg-response.el b/generic/pg-response.el index 015b111a..a1058f18 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -275,7 +275,8 @@ Returns non-nil if response buffer was cleared." (defun pg-response-display (str) "Show STR as a response in the response buffer." - (unless pg-use-specials-for-fontify + (unless (or proof-shell-unicode + pg-use-specials-for-fontify) (setq str (pg-assoc-strip-subterm-markup str))) (proof-shell-maybe-erase-response t nil) ;;(unless (or (string-equal str "") (string-equal str "\n")) |