aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2005-09-14 19:11:48 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2005-09-14 19:11:48 +0000
commit394911bf19147112dd86060c902693ce7e1dc48b (patch)
treeea5bebd5eea41699ea61d72f8b1c06d923db62c6 /isa
parentf255d4fecb737a56c9c8c5a59985449ed0e864ca (diff)
removed 8bit special chars for isar;
Diffstat (limited to 'isa')
-rw-r--r--isa/x-symbol-isabelle.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index eb6facb7..a5fe0126 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -113,7 +113,9 @@ or subscript tag."
;; the [\350-\357].\350\\|\^A[A-H].\^AA part is there to enable single
;; char sub/super scripts with coloured Isabelle output.
(defcustom x-symbol-isabelle-single-char-regexp
- "[\350-\357].\350\\|\^A[A-H].\^AA\\|[^\\]\\|\\\\\\\\?<[A-Za-z0-9_']+>"
+ (if (eq proof-assistant-symbol 'isar)
+ "\^A[A-H].\^AA\\|[^\\]\\|\\\\<[A-Za-z0-9_']+>"
+ "[\350-\357].\350\\|\^A[A-H].\^AA\\|[^\\]\\|\\\\\\\\?<[A-Za-z0-9_']+>")
"Return regexp matching \<ident> or c for some char c."
:group 'x-symbol-isabelle
:type 'regexp)