2 files changed, 77 insertions, 3 deletions
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 7c1b09b2..95c4b691 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -41,7 +41,8 @@
      token-match
      hexcode-match
      token-prefix
-     token-suffix))
+     token-suffix
+     shortcut-alist))
   (unicode-tokens-initialise)
   (setq proof-unicode-tokens-initialised t))
   
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 0564d28f..414b926a 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -5,8 +5,10 @@
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
 ;; This file is loaded by `proof-unicode-tokens.el'.
-;; It sets the variables defined at the top of unicode-tokens.el.
-;; unicode-tokens-<foo> is set from isar-<foo>.
+;;
+;; It sets the variables defined at the top of unicode-tokens.el,
+;; unicode-tokens-<foo> is set from isar-<foo>.  See the corresponding
+;; variable for documentation.
 ;;
 
 (defconst isar-token-format "\\<%s>")
@@ -303,6 +305,77 @@
    ("ffl" . "ﬄ")
    ))
 
+(defvar isar-shortcut-alist
+  '(; short cut, unicode string
+    ("<>" . "⋄")
+    ("|>" . "⊳")
+    ("\\/" . "∨")
+    ("/\\" . "∧")
+    ("+O" . "⊕")
+    ("-O" . "⊖")
+    ("xO" . "⊗")
+    ("/O" . "⊘")
+    (".O" . "⊙")
+    ("|+" . "†")
+    ("|++" . "‡")
+    ("<=" . "≤")
+    ("|-" . "⊢")
+    (">=" . "≥")
+    ("-|" . "⊣")
+    ("||" . "∥")
+    ("==" . "≡")
+    ("~=" . "≃")
+    ("~~~" . "≍")
+    ("~~" . "≈")
+    ("~==" . "≅")
+    ("|<>|" . "⋈")
+    ("|=" . "⊨")
+    ("=." . "≐")
+    ("_|_" . "⊥")
+    ("</" . "≮")
+    (">=/" . "≱")
+    ("=/" . "≠")
+    ("==/" . "≢")
+    ("~/" . "≁")
+    ("~=/" . "≄")
+    ("~~/" . "≉")
+    ("~==/" . "≇")
+    ("<-" . "←")
+    ("<=" . "⇐")
+    ("->" . "→")
+    ("=>" . "⇒")
+    ("<->" . "↔")
+    ("<=>" . "⇔")
+    ("|->" . "↦")
+    ("<--" . "⟵")
+    ("<==" . "⟸")
+    ("-->" . "⟶")
+    ("==>" . "⟹")
+    ("<==>" . "⟷")
+    ("|-->" . "⟼")
+    ("<--" . "←⎯")
+    ("<-->" . "⟷")
+    ("<<" . "⟪")
+    ("[|" . "⟦")
+    (">>" . "⟫")
+    ("|]" . "⟧")
+    ("``" . "”")
+    ("''" . "“")
+    ("--" . "–")
+    ("---" . "—")
+    ("''" . "″")
+    ("'''" . "‴")
+    ("''''" . "⁗")
+    ("nat" . "ℕ")
+    ("int" . "ℤ")
+    ("rat" . "ℚ")
+    ("real" . "ℝ")
+    ("complex" . "ℂ")
+    (":=" . "≔")
+    ("euro" . "€")
+    ("yen" . "¥")
+    ("cent" . "¢")))
+
 
 (provide 'isar-unicode-tokens)