backport of recent changes to isar-unicode-tokens.el:

more precise regexps isar-token-match, isar-control-token-match;
isar-shortcut-alist: map << >> to guillemots -- this is what HOL-Nominal expects;
isar-shortcut-alist: tweaked behaviour of ~= ~: <= `` which all have a particular meaning in Isabelle;
add back |-> shortcut;

1 files changed, 10 insertions, 8 deletions

diff --git a/isar/isar-unicode-tokens2.el b/isar/isar-unicode-tokens2.el
index 67615b7d..20b77c0b 100644
--- a/isar/isar-unicode-tokens2.el
+++ b/isar/isar-unicode-tokens2.el
@@ -15,8 +15,8 @@
 (defconst isar-charref-format "\\<#x%x>")
 (defconst isar-token-prefix "\\<")
 (defconst isar-token-suffix ">")
-(defconst isar-token-match "\\\\<\\([a-zA-Z0-9]+\\)")
-(defconst isar-control-token-match "\\\\<^\\([a-zA-Z0-9]+\\)>")
+(defconst isar-token-match "\\\\<\\([a-zA-Z][a-zA-Z0-9_']+\\)>")
+(defconst isar-control-token-match "\\\\<^\\([a-zA-Z][a-zA-Z0-9_']+\\)>")
 (defconst isar-control-token-format "\\<^%s>")
 (defconst isar-hexcode-match "\\\\<\\(#[xX][0-9A-Fa-f]+\\)")
 (defconst isar-next-character-regexp "\\\\<#[xX][0-9A-Fa-f]+>\\|.")
@@ -508,7 +508,9 @@ results will be undefined when files are saved."
     ("-|" . "⊣")
     ("||" . "∥")
     ("==" . "≡")
-    ("~=" . "≃")
+    ("~=" . "≠")
+    ("~:" . "∉")
+;    ("~=" . "≃")
     ("~~~" . "≍")
     ("~~" . "≈")
     ("~==" . "≅")
@@ -525,12 +527,12 @@ results will be undefined when files are saved."
     ("~~/" . "≉")
     ("~==/" . "≇")
     ("<-" . "←")
-    ("<=" . "⇐")
+;    ("<=" . "⇐")
     ("->" . "→")
     ("=>" . "⇒")
     ("<->" . "↔")
     ("<=>" . "⇔")
-;    ("|->" . "↦") 
+    ("|->" . "↦") 
     ("<--" . "⟵")
     ("<==" . "⟸")
     ("-->" . "⟶")
@@ -538,11 +540,11 @@ results will be undefined when files are saved."
     ("<==>" . "⟷")
     ("|-->" . "⟼")
     ("<-->" . "⟷")
-    ("<<" . "⟪")
+    ("<<" . "«")
     ("[|" . "⟦")
-    (">>" . "⟫")
+    (">>" . "»")
     ("|]" . "⟧")
-    ("``" . "”")
+;    ("``" . "”")
 ;    ("''" . "“")
 ;    ("--" . "–")
     ("---" . "—")