1(global-set-key (kbd "C-!") "���") 2(global-set-key (kbd "C-?") "���") 3(global-set-key (kbd "C-&") "���") 4(global-set-key (kbd "C-|") "���") 5(global-set-key (kbd "C->") "���") 6(global-set-key (kbd "C-<") "���") 7(global-set-key (kbd "C-M->") "���") 8(global-set-key (kbd "C-+") "���") 9(global-set-key (kbd "C-M-+") "���") 10(global-set-key (kbd "C-S-u") "���") 11(global-set-key (kbd "C-S-i") "���") 12(global-set-key (kbd "C-:") "���") 13(global-set-key (kbd "C-~") (lambda () (interactive) (insert "��"))) 14(global-set-key (kbd "C-S-c") "���") 15(global-set-key (kbd "C-S-q") "���") 16(global-set-key (kbd "C-M-~") "���") 17 18(global-set-key (kbd "C-{") "���") 19(global-set-key (kbd "C-}") "���") 20(global-set-key (kbd "C-M-{") "���") 21(global-set-key (kbd "C-M-}") "���") 22 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) 50 51;; Greek : C-S-<char> for lower case version of Greek <char> 52;; add the Meta modifier for upper case Greek letter. 53(global-set-key (kbd "C-S-a") "��") 54(global-set-key (kbd "C-S-b") "��") 55(global-set-key (kbd "C-S-g") "��") 56(global-set-key (kbd "C-S-d") "��") 57(global-set-key (kbd "C-S-e") "��") 58(global-set-key (kbd "C-S-l") "��") 59(global-set-key (kbd "C-S-m") "��") 60(global-set-key (kbd "C-S-n") "��") 61(define-key hol-unicode-p-map "i" "��") 62(global-set-key (kbd "C-S-o") "��") 63(global-set-key (kbd "C-S-r") "��") 64(global-set-key (kbd "C-S-s") "��") 65(global-set-key (kbd "C-S-t") "��") 66(global-set-key (kbd "C-S-x") "��") 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" "��") 70 71(global-set-key (kbd "C-S-M-g") "��") 72(global-set-key (kbd "C-S-M-d") "��") 73(global-set-key (kbd "C-S-M-l") "��") 74(global-set-key (kbd "C-S-M-s") "��") 75(global-set-key (kbd "C-S-M-t") "��") 76(global-set-key (kbd "C-S-M-o") "��") 77(global-set-key (kbd "C-S-M-x") "��") 78(define-key hol-unicode-P-map "i" "��") 79(define-key hol-unicode-P-map "h" "��") 80(define-key hol-unicode-P-map "s" "��") 81 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 ",") "���") 91 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 "-" "���") 122 123(define-key hol-unicode-superscript-map "1" 124 (lambda () (interactive) (insert "��"))) 125(define-key hol-unicode-superscript-map "2" 126 (lambda () (interactive) (insert "��"))) 127(define-key hol-unicode-superscript-map "3" 128 (lambda () (interactive) (insert "��"))) 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 "=" "���") 139 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" "���") 184 185;; ��� ��� ��� ��� ��� ��� ��� ��� ��� ��� ��� ��� ��� 186 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 195 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 200 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-]") "���") 214 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") "���") 219 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 "<") "���") 229 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-<") 234 (lambda () (interactive) (insert "��"))) 235(define-key hol-unicode-dquote-map (kbd "C-M->") 236 (lambda () (interactive) (insert "��"))) 237 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-<") 242 (lambda () (interactive) (insert "���"))) 243(define-key hol-unicode-squote-map (kbd "C->") 244 (lambda () (interactive) (insert "���"))) 245 246(define-key hol-unicode-specialalphabet-map (kbd "f") hol-unicode-frak-map) 247; fraktur map 248; app (fn (s1,s2,s3) => 249; print ("(define-key hol-unicode-frak-map (kbd \"" ^ s1 ^ "\") \"" ^ 250; s2 ^ "\") ; U+" ^ s3 ^ "\n")) 251; (List.tabulate (26, (fn i => (UTF8.chr (i + 65), 252; UTF8.chr (i + 0x1D56C), 253; Int.fmt StringCvt.HEX (i + 0x1D56C))))); 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 280; app (fn (s1,s2,s3) => 281; print ("(define-key hol-unicode-frak-map (kbd \"" ^ s1 ^ "\") \"" ^ 282; s2 ^ "\") ; U+" ^ s3 ^ "\n")) 283; (List.tabulate (26, (fn i => (UTF8.chr (i + 97), 284; UTF8.chr (i + 0x1D586), 285; Int.fmt StringCvt.HEX (i + 0x1D586))))); 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 312