From cfed30e1257a7d18a7e8675d7d099bf469ccb1ce Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 14 Dec 2007 00:43:03 +0000
Subject: Make value of pg-special-char-regexp depend on proof-shell-unicode.
 This makes sure that stripping special characters from output is accurate.

---
 isar/isar.el | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index 16384979..f154c711 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -211,12 +211,13 @@ See -k option for Isabelle interface script."
    ;; Allow font-locking for output based on hidden annotations, see
    ;; isar-output-font-lock-keywords-1
    pg-use-specials-for-fontify		t
+   pg-after-fontify-output-hook	        'pg-remove-specials
+
    pg-special-char-regexp
+   (if proof-shell-unicode "
[0-9A-Z]"
+     ;; next string could be: "[\350-\377]", but that's buggy with XEmacs 21.5 (beta)
+     "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|")
 
-   ;; should be: "[\350-\377]\\|\^A[A-Z]", but literal chars
-   ;; prevent problems with XEmacs 21.5 (beta)
-   "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|
[0-9A-Z]"
-   pg-after-fontify-output-hook	        'pg-remove-specials
    pg-subterm-help-cmd			"term %s" 
 
    proof-cannot-reopen-processed-files  t
-- 
cgit v1.2.3