From 7755773c265b784a7ca55f3413b7ee14f345d2ee Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 28 Jan 2008 13:29:53 +0000
Subject: Support decoding of unicode tokens in output

---
 generic/proof-utils.el | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index b7c2c482..531b7fa0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -384,6 +384,8 @@ font-lock-mode; in those buffers, we enable syntactic fontification also."
 Fontifies (keywords only) according to the buffer's font lock defaults.
 Uses `proof-x-symbol-decode-region' to decode tokens
 if X-Symbol is enabled.
+Uses `unicode-tokens-tokens-to-unicode' to decode tokens
+if unicode symbols are enabled.
 
 If `pg-use-specials-for-fontify' is set, remove characters
 with top bit set after fontifying so they don't spoil cut and paste,
@@ -431,8 +433,11 @@ Returns new END value."
 	(setq end (point-max)))
 
       (prog1 ;; prog1 because we return new END value.
-	  (if (proof-ass x-symbol-enable)
-	      (proof-x-symbol-decode-region start end))
+	  (cond
+	   ((proof-ass x-symbol-enable)
+	    (proof-x-symbol-decode-region start end))
+	   ((proof-ass unicode-tokens-enable)
+	    (unicode-tokens-tokens-to-unicode start end)))
 	(proof-font-lock-clear-font-lock-vars)
 	(setq font-lock-verbose normal-font-lock-verbose)))))
 
-- 
cgit v1.2.3