blob: e03ae0d3b5010d721f0b4398b2c5b98ebbff782b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
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
|
