HOL4/tools/hol-unicode.el

23 (define-prefix-command 'hol-unicode-p-map)
24 (define-prefix-command 'hol-unicode-P-map)
25 (define-prefix-command 'hol-unicode-not-map)
26 (define-prefix-command 'hol-unicode-subscript-map)
27 (define-prefix-command 'hol-unicode-superscript-map)
28 (define-prefix-command 'hol-unicode-C-map)
29 (define-prefix-command 'hol-unicode-U-map)
30 (define-prefix-command 'hol-unicode-lparen-map)
31 (define-prefix-command 'hol-unicode-rparen-map)
32 (define-prefix-command 'hol-unicode-shift-map)
33 (define-prefix-command 'hol-unicode-dquote-map)
34 (define-prefix-command 'hol-unicode-squote-map)
35 (define-prefix-command 'hol-unicode-frak-map)
36 (define-prefix-command 'hol-unicode-specialalphabet-map)
37 (define-key global-map (kbd "C-S-f") 'hol-unicode-shift-map)
38 (define-key global-map (kbd "C-S-p") 'hol-unicode-p-map)
39 (define-key global-map (kbd "C-M-S-p") 'hol-unicode-P-map)
40 (define-key global-map (kbd "C-M-|") 'hol-unicode-not-map)
41 (define-key global-map (kbd "C-M-_") 'hol-unicode-subscript-map)
42 (define-key global-map (kbd "C-M-^") 'hol-unicode-superscript-map)
43 (define-key global-map (kbd "C-S-M-c") 'hol-unicode-C-map)
44 (define-key global-map (kbd "C-S-M-u") 'hol-unicode-U-map)
45 (define-key global-map (kbd "C-M-(") 'hol-unicode-lparen-map)
46 (define-key global-map (kbd "C-M-)") 'hol-unicode-rparen-map)
47 (define-key global-map (kbd "C-\"") 'hol-unicode-squote-map)
48 (define-key global-map (kbd "C-M-\"") 'hol-unicode-dquote-map)
49 (define-key global-map (kbd "C-M-a") 'hol-unicode-specialalphabet-map)
61 (define-key hol-unicode-p-map "i" "��")
67 (define-key hol-unicode-p-map "h" "��")  ; U+03D5
68 (define-key hol-unicode-p-map "v" "��")  ; U+03C6
69 (define-key hol-unicode-p-map "s" "��")
78 (define-key hol-unicode-P-map "i" "��")
79 (define-key hol-unicode-P-map "h" "��")
80 (define-key hol-unicode-P-map "s" "��")
82 (define-key hol-unicode-not-map "=" "���")
83 (define-key hol-unicode-not-map ":" "���")
84 (define-key hol-unicode-not-map "0" "���")
85 (define-key hol-unicode-not-map "~" "���")
86 (define-key hol-unicode-not-map "<" "���")
87 (define-key hol-unicode-not-map ">" "���")
88 (define-key hol-unicode-not-map (kbd "C-S-q") "���")
89 (define-key hol-unicode-not-map (kbd "C-+") "���")
90 (define-key hol-unicode-not-map (kbd ",") "���")
92 (define-key hol-unicode-subscript-map "1" "���")
93 (define-key hol-unicode-subscript-map "2" "���")
94 (define-key hol-unicode-subscript-map "3" "���")
95 (define-key hol-unicode-subscript-map "4" "���")
96 (define-key hol-unicode-subscript-map "5" "���")
97 (define-key hol-unicode-subscript-map "6" "���")
98 (define-key hol-unicode-subscript-map "7" "���")
99 (define-key hol-unicode-subscript-map "8" "���")
100 (define-key hol-unicode-subscript-map "9" "���")
101 (define-key hol-unicode-subscript-map "0" "���")
102 (define-key hol-unicode-subscript-map "a" "���")
103 (define-key hol-unicode-subscript-map "e" "���")
104 (define-key hol-unicode-subscript-map "h" "���")
105 (define-key hol-unicode-subscript-map "i" "���")
106 (define-key hol-unicode-subscript-map "j" "���")
107 (define-key hol-unicode-subscript-map "k" "���")
108 (define-key hol-unicode-subscript-map "l" "���")
109 (define-key hol-unicode-subscript-map "m" "���")
110 (define-key hol-unicode-subscript-map "n" "���")
111 (define-key hol-unicode-subscript-map "o" "���")
112 (define-key hol-unicode-subscript-map "p" "���")
113 (define-key hol-unicode-subscript-map "r" "���")
114 (define-key hol-unicode-subscript-map "s" "���")
115 (define-key hol-unicode-subscript-map "t" "���")
116 (define-key hol-unicode-subscript-map "u" "���")
117 (define-key hol-unicode-subscript-map "v" "���")
118 (define-key hol-unicode-subscript-map "x" "���")
119 (define-key hol-unicode-subscript-map "+" "���")
120 (define-key hol-unicode-subscript-map "=" "���")
121 (define-key hol-unicode-subscript-map "-" "���")
123 (define-key hol-unicode-superscript-map "1"
125 (define-key hol-unicode-superscript-map "2"
127 (define-key hol-unicode-superscript-map "3"
129 (define-key hol-unicode-superscript-map "4" "���")
130 (define-key hol-unicode-superscript-map "5" "���")
131 (define-key hol-unicode-superscript-map "6" "���")
132 (define-key hol-unicode-superscript-map "7" "���")
133 (define-key hol-unicode-superscript-map "8" "���")
134 (define-key hol-unicode-superscript-map "9" "���")
135 (define-key hol-unicode-superscript-map "0" "���")
136 (define-key hol-unicode-superscript-map "+" "���")
137 (define-key hol-unicode-superscript-map "-" "���")
138 (define-key hol-unicode-superscript-map "=" "���")
140 (define-key hol-unicode-superscript-map "A" "���")
141 (define-key hol-unicode-superscript-map "B" "���")
142 (define-key hol-unicode-superscript-map "D" "���")
143 (define-key hol-unicode-superscript-map "E" "���")
144 (define-key hol-unicode-superscript-map "G" "���")
145 (define-key hol-unicode-superscript-map "H" "���")
146 (define-key hol-unicode-superscript-map "I" "���")
147 (define-key hol-unicode-superscript-map "J" "���")
148 (define-key hol-unicode-superscript-map "K" "���")
149 (define-key hol-unicode-superscript-map "L" "���")
150 (define-key hol-unicode-superscript-map "M" "���")
151 (define-key hol-unicode-superscript-map "N" "���")
152 (define-key hol-unicode-superscript-map "O" "���")
153 (define-key hol-unicode-superscript-map "P" "���")
154 (define-key hol-unicode-superscript-map "R" "���")
155 (define-key hol-unicode-superscript-map "T" "���")
156 (define-key hol-unicode-superscript-map "U" "���")
157 (define-key hol-unicode-superscript-map "V" "���")
158 (define-key hol-unicode-superscript-map "W" "���")
159 (define-key hol-unicode-superscript-map "a" "���")
160 (define-key hol-unicode-superscript-map "b" "���")
161 (define-key hol-unicode-superscript-map "c" "���")
162 (define-key hol-unicode-superscript-map "d" "���")
163 (define-key hol-unicode-superscript-map "e" "���")
164 (define-key hol-unicode-superscript-map "f" "���")
165 (define-key hol-unicode-superscript-map "g" "���")
166 (define-key hol-unicode-superscript-map "h" "��")
167 (define-key hol-unicode-superscript-map "i" "���")
168 (define-key hol-unicode-superscript-map "j" "��")
169 (define-key hol-unicode-superscript-map "k" "���")
170 (define-key hol-unicode-superscript-map "l" "��")
171 (define-key hol-unicode-superscript-map "m" "���")
172 (define-key hol-unicode-superscript-map "n" "���")
173 (define-key hol-unicode-superscript-map "o" "���")
174 (define-key hol-unicode-superscript-map "p" "���")
175 (define-key hol-unicode-superscript-map "r" "��")
176 (define-key hol-unicode-superscript-map "s" "��")
177 (define-key hol-unicode-superscript-map "t" "���")
178 (define-key hol-unicode-superscript-map "u" "���")
179 (define-key hol-unicode-superscript-map "v" "���")
180 (define-key hol-unicode-superscript-map "w" "��")
181 (define-key hol-unicode-superscript-map "x" "��")
182 (define-key hol-unicode-superscript-map "y" "��")
183 (define-key hol-unicode-superscript-map "z" "���")
187 (define-prefix-command 'hol-unicode-zero-map)
188 (global-set-key (kbd "C-)") 'hol-unicode-zero-map)
189 (define-key hol-unicode-zero-map "+" "���")
190 (define-key hol-unicode-zero-map "*" "���")
191 (define-key hol-unicode-zero-map "-" "���")
192 (define-key hol-unicode-zero-map "." "���")
193 (define-key hol-unicode-zero-map "/" "���")
194 (define-key hol-unicode-zero-map "0" "���") ; U+2218
196 (define-key hol-unicode-U-map "u" "����")
197 (define-key hol-unicode-U-map "+" "���") ; U+228E "multiset union"
198 (define-key hol-unicode-U-map "<" "���") ; U+228C called simply "multiset", used in HOL for FUNION
199 (define-key hol-unicode-U-map "p" "��") ; Up-silon
201 ; parenthesis map - for various forms of parenthesis
202 (define-key hol-unicode-lparen-map (kbd "C-M-|") "���")
203 (define-key hol-unicode-rparen-map (kbd "C-M-|") "���")
204 (define-key hol-unicode-lparen-map (kbd "C-M-(") "���")
205 (define-key hol-unicode-rparen-map (kbd "C-M-)") "���")
206 (define-key hol-unicode-lparen-map (kbd "C-<") "���")
207 (define-key hol-unicode-rparen-map (kbd "C->") "���")
208 (define-key hol-unicode-lparen-map (kbd "C-M-<") "���")
209 (define-key hol-unicode-rparen-map (kbd "C-M->") "���")
210 (define-key hol-unicode-lparen-map (kbd "C-M-^") "���")
211 (define-key hol-unicode-rparen-map (kbd "C-M-^") "���")
212 (define-key hol-unicode-lparen-map (kbd "C-M-[") "���")
213 (define-key hol-unicode-rparen-map (kbd "C-M-]") "���")
215 ; shift map
216 (define-key hol-unicode-shift-map (kbd "a") "���")
217 (define-key hol-unicode-shift-map (kbd "l") "���")
218 (define-key hol-unicode-shift-map (kbd "r") "���")
220 ; curly/curvy relational operator map
221 (define-key hol-unicode-C-map (kbd "_") "���")
222 (define-key hol-unicode-C-map (kbd "-") "���")
223 (define-key hol-unicode-C-map (kbd ".") "���")
224 (define-key hol-unicode-C-map (kbd "c") "���")
225 (define-key hol-unicode-C-map (kbd "p") "���")  ; "p" for proper
226 (define-key hol-unicode-C-map (kbd "q") "���")  ; "q" for less-or-eQual
227 (define-key hol-unicode-C-map (kbd "=") "���")
228 (define-key hol-unicode-C-map (kbd "<") "���")
230 ; double quotation marks map
231 (define-key hol-unicode-dquote-map (kbd "C-M-{") "���")
232 (define-key hol-unicode-dquote-map (kbd "C-M-}") "���")
233 (define-key hol-unicode-dquote-map (kbd "C-M-<")
235 (define-key hol-unicode-dquote-map (kbd "C-M->")
238 ; single quotation marks map
239 (define-key hol-unicode-squote-map (kbd "C-{") "���")
240 (define-key hol-unicode-squote-map (kbd "C-}") "���")
241 (define-key hol-unicode-squote-map (kbd "C-<")
243 (define-key hol-unicode-squote-map (kbd "C->")
246 (define-key hol-unicode-specialalphabet-map (kbd "f") hol-unicode-frak-map)
247 ; fraktur map
249 ;        print ("(define-key hol-unicode-frak-map (kbd \"" ^ s1 ^ "\") \"" ^
254 (define-key hol-unicode-frak-map (kbd "A") "����")  ; U+1D56C
255 (define-key hol-unicode-frak-map (kbd "B") "����")  ; U+1D56D
256 (define-key hol-unicode-frak-map (kbd "C") "����")  ; U+1D56E
257 (define-key hol-unicode-frak-map (kbd "D") "����")  ; U+1D56F
258 (define-key hol-unicode-frak-map (kbd "E") "����")  ; U+1D570
259 (define-key hol-unicode-frak-map (kbd "F") "����")  ; U+1D571
260 (define-key hol-unicode-frak-map (kbd "G") "����")  ; U+1D572
261 (define-key hol-unicode-frak-map (kbd "H") "����")  ; U+1D573
262 (define-key hol-unicode-frak-map (kbd "I") "����")  ; U+1D574
263 (define-key hol-unicode-frak-map (kbd "J") "����")  ; U+1D575
264 (define-key hol-unicode-frak-map (kbd "K") "����")  ; U+1D576
265 (define-key hol-unicode-frak-map (kbd "L") "����")  ; U+1D577
266 (define-key hol-unicode-frak-map (kbd "M") "����")  ; U+1D578
267 (define-key hol-unicode-frak-map (kbd "N") "����")  ; U+1D579
268 (define-key hol-unicode-frak-map (kbd "O") "����")  ; U+1D57A
269 (define-key hol-unicode-frak-map (kbd "P") "����")  ; U+1D57B
270 (define-key hol-unicode-frak-map (kbd "Q") "����")  ; U+1D57C
271 (define-key hol-unicode-frak-map (kbd "R") "����")  ; U+1D57D
272 (define-key hol-unicode-frak-map (kbd "S") "����")  ; U+1D57E
273 (define-key hol-unicode-frak-map (kbd "T") "����")  ; U+1D57F
274 (define-key hol-unicode-frak-map (kbd "U") "����")  ; U+1D580
275 (define-key hol-unicode-frak-map (kbd "V") "����")  ; U+1D581
276 (define-key hol-unicode-frak-map (kbd "W") "����")  ; U+1D582
277 (define-key hol-unicode-frak-map (kbd "X") "����")  ; U+1D583
278 (define-key hol-unicode-frak-map (kbd "Y") "����")  ; U+1D584
279 (define-key hol-unicode-frak-map (kbd "Z") "����")  ; U+1D585
281 ;        print ("(define-key hol-unicode-frak-map (kbd \"" ^ s1 ^ "\") \"" ^
286 (define-key hol-unicode-frak-map (kbd "a") "����")  ; U+1D586
287 (define-key hol-unicode-frak-map (kbd "b") "����")  ; U+1D587
288 (define-key hol-unicode-frak-map (kbd "c") "����")  ; U+1D588
289 (define-key hol-unicode-frak-map (kbd "d") "����")  ; U+1D589
290 (define-key hol-unicode-frak-map (kbd "e") "����")  ; U+1D58A
291 (define-key hol-unicode-frak-map (kbd "f") "����")  ; U+1D58B
292 (define-key hol-unicode-frak-map (kbd "g") "����")  ; U+1D58C
293 (define-key hol-unicode-frak-map (kbd "h") "����")  ; U+1D58D
294 (define-key hol-unicode-frak-map (kbd "i") "����")  ; U+1D58E
295 (define-key hol-unicode-frak-map (kbd "j") "����")  ; U+1D58F
296 (define-key hol-unicode-frak-map (kbd "k") "����")  ; U+1D590
297 (define-key hol-unicode-frak-map (kbd "l") "����")  ; U+1D591
298 (define-key hol-unicode-frak-map (kbd "m") "����")  ; U+1D592
299 (define-key hol-unicode-frak-map (kbd "n") "����")  ; U+1D593
300 (define-key hol-unicode-frak-map (kbd "o") "����")  ; U+1D594
301 (define-key hol-unicode-frak-map (kbd "p") "����")  ; U+1D595
302 (define-key hol-unicode-frak-map (kbd "q") "����")  ; U+1D596
303 (define-key hol-unicode-frak-map (kbd "r") "����")  ; U+1D597
304 (define-key hol-unicode-frak-map (kbd "s") "����")  ; U+1D598
305 (define-key hol-unicode-frak-map (kbd "t") "����")  ; U+1D599
306 (define-key hol-unicode-frak-map (kbd "u") "����")  ; U+1D59A
307 (define-key hol-unicode-frak-map (kbd "v") "����")  ; U+1D59B
308 (define-key hol-unicode-frak-map (kbd "w") "����")  ; U+1D59C
309 (define-key hol-unicode-frak-map (kbd "x") "����")  ; U+1D59D
310 (define-key hol-unicode-frak-map (kbd "y") "����")  ; U+1D59E
311 (define-key hol-unicode-frak-map (kbd "z") "����")  ; U+1D59F