;;; 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