diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:21:14 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 10:21:14 +0000 |
commit | db570710763e4209ee7e0b093e6bbb73ca48cb2f (patch) | |
tree | a2127242241efeadf969bc530144d7235e7b2289 | |
parent | 6224291b429b170ca6e2c590fc0870cb7cfd3cf8 (diff) |
isar-control-char-format-regexp: correct to only affect next char/symbol
isar-control-regions: add \<^bisup>..\<^eisup> and \<^bisub>..\<^eisub>
-rw-r--r-- | isar/isar-unicode-tokens.el | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index c8e50679..3241234c 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -46,15 +46,7 @@ (defconst isar-control-char-format-regexp (concat "\\(\\\\<\\^%s>\\)\\(" -; isar-long-id-stuff: - "\\(?:" -; "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z0-9'_]\\)" -; apparently wrong: subscripts \\<^isub>____x\\<^isub>y____ - "\\(?:\\\\<[A-Za-z]+>\\|[A-Za-z0-9'_]\\)" - "\\|\\.\\)+" - "\\|[^\\]" - ;; above was simply: \\\\<[A-Za-z]+> - "\\|[^\\]" + "\\(?:\\\\<[A-Za-z]+>\\|[^\\]\\)" ; cf isar-ext-first "\\)")) (defconst isar-control-char-format "\\<^%s>") @@ -70,7 +62,7 @@ ("Loc" "loc" keyword) ("Constant" "const" keyword) ("Bold" "bold" bold) - ;; unofficial: + ;; unofficial/unsupported: ("Italic" "italic" italic)) "Control character tokens for Isabelle." :group 'isabelle-tokens @@ -79,7 +71,9 @@ (defcustom isar-control-regions '(("Subscript" "bsub" "esub" sub) ("Superscript" "bsup" "esup" sup) - ;; unofficial: + ;; unofficial/unsupported: + ("Id subscript" "bisub" "eisub" sub) + ("Id superscript" "bisup" "eisup" sup) ("Bold" "bbold" "ebold" bold) ("Italic" "bitalic" "eitalic" italic) ("Script" "bscript" "escript" script) |