diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 10:38:55 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 10:38:55 +0000 |
| commit | a8e8ffa54ac578e5657853bd163c5b09a313f178 (patch) | |
| tree | 45c798555c2f7ccbc8a744ef56ca88cf06cbba17 /generic | |
| parent | f60e5be1803cd30f9030a1a432d8a64561882f35 (diff) | |
Use proof-shell-unicode to control whether bytes 128-255 are stripped from output.
Diffstat (limited to 'generic')
| -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")) |