diff options
| author | David Aspinall | 2007-12-14 00:43:03 +0000 |
|---|---|---|
| committer | David Aspinall | 2007-12-14 00:43:03 +0000 |
| commit | cfed30e1257a7d18a7e8675d7d099bf469ccb1ce (patch) | |
| tree | 2780f6aea1d9d9ba7885f8fa5999a1c28fbda4ff /isar | |
| parent | 780d48143f5d91f3074ba1334d6b6cc8ab852c02 (diff) | |
Make value of pg-special-char-regexp depend on proof-shell-unicode.
This makes sure that stripping special characters from output is accurate.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 9 |
1 files 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 |