From a8e8ffa54ac578e5657853bd163c5b09a313f178 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 14 Dec 2007 10:38:55 +0000 Subject: Use proof-shell-unicode to control whether bytes 128-255 are stripped from output. --- generic/pg-goals.el | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'generic/pg-goals.el') 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 -- cgit v1.2.3