diff options
| author | Makarius Wenzel | 2005-09-01 14:18:11 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2005-09-01 14:18:11 +0000 |
| commit | 825242347d4582515121b1372eaab62e57c98209 (patch) | |
| tree | abdcf0c1e22230026bff5072530212095f2be8a1 | |
| parent | 73375b71d50c9be41127d424b4868a5d0ccdba80 (diff) | |
special regexps: include PGASCII version;
| -rw-r--r-- | isa/x-symbol-isabelle.el | 6 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 10 |
2 files changed, 13 insertions, 3 deletions
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el index f4ee80dd..eb6facb7 100644 --- a/isa/x-symbol-isabelle.el +++ b/isa/x-symbol-isabelle.el @@ -110,10 +110,10 @@ or subscript tag." :type 'regexp) -;; the [\350-\360].\350 part is there to enable single char sub/super scripts -;; with coloured Isabelle output. +;; 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-\360].\350\\|[^\\]\\|\\\\\\\\?<[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) diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 3fb71556..314d0837 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -368,6 +368,16 @@ matches contents of quotes for quoted identifiers.") (cons (concat "\356\\?" isar-idx "\350") 'isabelle-var-name-face) (cons (concat "\357" isar-id "\350") 'proof-declaration-name-face) (cons (concat "\357\\?" isar-idx "\350") 'proof-declaration-name-face) + (cons (concat "\^AB" isar-long-id-stuff "\^AA") 'isabelle-class-name-face) + (cons (concat "\^AC'" isar-id "\^AA") 'isabelle-tfree-name-face) + (cons (concat "\^AD'" isar-idx "\^AA") 'isabelle-tvar-name-face) + (cons (concat "\^AD\\?'" isar-idx "\^AA") 'isabelle-tvar-name-face) + (cons (concat "\^AE" isar-id "\^AA") 'isabelle-free-name-face) + (cons (concat "\^AF" isar-id "\^AA") 'isabelle-bound-name-face) + (cons (concat "\^AG" isar-idx "\^AA") 'isabelle-var-name-face) + (cons (concat "\^AG\\?" isar-idx "\^AA") 'isabelle-var-name-face) + (cons (concat "\^AH" isar-id "\^AA") 'proof-declaration-name-face) + (cons (concat "\^AH\\?" isar-idx "\^AA") 'proof-declaration-name-face) isar-font-lock-local) "*Font-lock table for Isabelle terms.") |