1 files changed, 124 insertions, 0 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
new file mode 100644
index 00000000..e03ae0d3
--- /dev/null
+++ b/isar/isar-unicode-tokens.el
@@ -0,0 +1,124 @@
+;;; isar-unicode-tokens.el --- Tokens for Unicode Tokens package
+;;
+;; Copyright(C) 2008 David Aspinall / LFCS Edinburgh
+;; 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>.
+;;
+
+(defconst isar-token-format "\\<%s>")
+(defconst isar-charref-format "\\<#x%x>")
+(defconst isar-token-prefix "\\<")
+(defconst isar-token-suffix ">")
+(defconst isar-token-match "\\\\<\\([a-zA-Z0-9]+\\)")
+(defconst isar-hexcode-match "\\\\<\\(#[xX][0-9A-Fa-f]+\\)")
+
+(defconst isar-token-name-alist
+  ;; Standard Unicode character names, see unicode-chars.el 
+  '(("spacespace" . "SYMBOL FOR SPACE")
+    ("Gamma" . "GREEK CAPITAL LETTER GAMMA")
+    ("Delta" . "GREEK CAPITAL LETTER DELTA")
+    ("Theta" . "GREEK CAPITAL LETTER THETA")
+    ("Lambda" . "GREEK CAPITAL LETTER LAMDA")
+    ("Pi" . "GREEK CAPITAL LETTER PI")
+    ("Sigma" . "GREEK CAPITAL LETTER SIGMA")
+    ("Phi" . "GREEK CAPITAL LETTER PHI")
+    ("Psi" . "GREEK CAPITAL LETTER PSI")
+    ("Omega" . "GREEK CAPITAL LETTER OMEGA")
+    ("alpha" . "GREEK SMALL LETTER ALPHA")
+    ("beta" . "GREEK SMALL LETTER BETA")
+    ("gamma" . "GREEK SMALL LETTER GAMMA")
+    ("delta" . "GREEK SMALL LETTER DELTA")
+    ("epsilon" . "GREEK SMALL LETTER EPSILON")
+    ("zeta" . "GREEK SMALL LETTER ZETA")
+    ("eta" . "GREEK SMALL LETTER ETA")
+    ("theta" . "GREEK SMALL LETTER THETA")
+    ("kappa" . "GREEK SMALL LETTER KAPPA")
+    ("lambda" . "GREEK SMALL LETTER LAMDA")
+    ("mu" . "GREEK SMALL LETTER MU")
+    ("nu" . "GREEK SMALL LETTER NU")
+    ("xi" . "GREEK SMALL LETTER XI")
+    ("pi" . "GREEK SMALL LETTER PI")
+    ("rho" . "GREEK SMALL LETTER RHO")
+    ("sigma" . "GREEK SMALL LETTER SIGMA")
+    ("tau" . "GREEK SMALL LETTER TAU")
+    ("phi" . "GREEK SMALL LETTER PHI")
+    ("chi" . "GREEK SMALL LETTER CHI")
+    ("psi" . "GREEK SMALL LETTER PSI")
+    ("omega" . "GREEK SMALL LETTER OMEGA")
+    ("not" . "NOT SIGN")
+    ("and" . "LOGICAL AND")
+    ("or" . "LOGICAL OR")
+    ("forall" . "FOR ALL")
+    ("exists" . "THERE EXISTS")
+    ("some" . "GREEK SMALL LETTER EPSILON")
+    ("And" . "N-ARY LOGICAL AND")
+    ("lceil" . "LEFT CEILING")
+    ("rceil" . "RIGHT CEILING")
+    ("lfloor" . "LEFT FLOOR")
+    ("rfloor" . "RIGHT FLOOR")
+    ("turnstile" . "RIGHT TACK")
+    ("Turnstile" . "TRUE")
+    ("lbrakk" . "LEFT WHITE SQUARE BRACKET")
+    ("rbrakk" . "RIGHT WHITE SQUARE BRACKET")
+    ("cdot" . "MIDDLE DOT")
+    ("in" . "ELEMENT OF")
+    ("subseteq" . "SUBSET OF OR EQUAL TO")
+    ("inter" . "INTERSECTION")
+    ("union" . "UNION")
+    ("Inter" . "N-ARY INTERSECTION")
+    ("Union" . "N-ARY UNION")
+    ("sqinter" . "SQUARE CAP")
+    ("squnion" . "SQUARE CUP")
+    ("Sqinter" . "N-ARY SQUARE INTERSECTION OPERATOR")
+    ("Squnion" . "N-ARY SQUARE UNION OPERATOR")
+    ("bottom" . "UP TACK")
+    ("doteq" . "IDENTICAL WITH DOT ABOVE")
+    ("wrong" . "WREATH PRODUCT")
+    ("equiv" . "IDENTICAL TO")
+    ("noteq" . "NOT EQUAL TO")
+    ("sqsubset" . "SQUARE IMAGE OF")
+    ("sqsubseteq" . "SQUARE IMAGE OF OR EQUAL TO")
+    ("prec" . "PRECEDES")
+    ("preceq" . "PRECEDES OR EQUAL TO")
+    ("succ" . "SUCCEEDS")
+    ("approx" . "APPROXIMATELY EQUAL TO")
+    ("sim" . "TILDE OPERATOR") ;; FIXME: check
+    ("simeq" . "ASYMPTOTICALLY EQUAL TO")
+    ("le" . "LESS-THAN OR EQUAL TO")
+    ("Colon" . "Z NOTATION TYPE COLON")
+    ("leftarrow" . "LEFTWARDS ARROW")
+    ("midarrow" . "EN DASH")
+    ("rightarrow" . "RIGHTWARDS ARROW")
+    ("Leftarrow" . "LEFTWARDS DOUBLE ARROW")
+;   (nil "\\<Midarrow>")
+    ("Rightarrow" . "RIGHTWARDS DOUBLE ARROW")
+    ("frown" . "FROWN")
+    ("mapsto" . "RIGHTWARDS ARROW FROM BAR")
+    ("leadsto" . "RIGHTWARDS SQUIGGLE ARROW")
+    ("up" . "UPWARDS ARROW")
+    ("down" . "DOWNWARDS ARROW")
+    ("notin" . "NOT AN ELEMENT OF")
+    ("times" . "MULTIPLICATION SIGN")
+    ("oplus" . "CIRCLED PLUS")
+    ("ominus" . "CIRCLED MINUS")
+    ("otimes" . "CIRCLED TIMES")
+    ("oslash" . "CIRCLED DIVISION SLASH")
+    ("subset" . "SUBSET OF")
+    ("infinity" . "INFINITY")
+    ("box" . "OPEN BOX")
+    ("diamond" . "DIAMOND OPERATOR")
+    ("circ" . "RING OPERATOR")
+    ("bullet" . "BULLET")
+    ("parallel" . "DOUBLE VERTICAL LINE")
+    ("surd" . "RADICAL SYMBOL BOTTOM")
+    ("copyright" . "COPYRIGHT SIGN")))
+
+
+
+
+(provide 'isar-unicode-tokens)
+
+;;; isar-unicode-tokens.el ends here