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/pg-goals.el | |
| parent | f60e5be1803cd30f9030a1a432d8a64561882f35 (diff) | |
Use proof-shell-unicode to control whether bytes 128-255 are stripped from output.
Diffstat (limited to 'generic/pg-goals.el')
| -rw-r--r-- | generic/pg-goals.el | 7 |
1 files changed, 5 insertions, 2 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 |