1;;; hol-input.el --- The Hol input method (based/copied from Lean) 2;;; 3;;; DISCLAIMER: This file is based on lean-input.el provided with the Lean theorem prover. 4;;; We did minor modifications 5;; 6;;; Commentary: 7;; 8;;;; A highly customisable input method which can inherit from other 9;; Quail input methods. By default the input method is geared towards 10;; the input of mathematical and other symbols in Hol programs. 11;; 12;; Use M-x customize-group hol-input to customise this input method. 13;; Note that the functions defined under "Functions used to tweak 14;; translation pairs" below can be used to tweak both the key 15;; translations inherited from other input methods as well as the 16;; ones added specifically for this one. 17;; 18;; Use hol-input-show-translations to see all the characters which 19;; can be typed using this input method (except for those 20;; corresponding to ASCII characters). 21 22;;; Code: 23 24(require 'quail) 25 26(eval-when-compile 27 (require 'cl)) 28;; Quail is quite stateful, so be careful when editing this code. Note 29;; that with-temp-buffer is used below whenever buffer-local state is 30;; modified. 31 32;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 33;; Utility functions 34 35(defun hol-input-concat-map (f xs) 36 "Concat (map F XS)." 37 (apply 'append (mapcar f xs))) 38 39(defun hol-input-to-string-list (s) 40 "Convert a string S to a list of one-character strings, after 41removing all space and newline characters." 42 (hol-input-concat-map 43 (lambda (c) (if (member c (string-to-list " \n")) 44 nil 45 (list (string c)))) 46 (string-to-list s))) 47 48(defun hol-input-character-range (from to) 49 "A string consisting of the characters from FROM to TO." 50 (let (seq) 51 (dotimes (i (1+ (- to from))) 52 (setq seq (cons (+ from i) seq))) 53 (concat (nreverse seq)))) 54 55;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 56;; Functions used to tweak translation pairs 57 58;; lexical-let is used since Elisp lacks lexical scoping. 59 60(defun hol-input-compose (f g) 61 "\x -> concatMap F (G x)" 62 (lexical-let ((f1 f) (g1 g)) 63 (lambda (x) (hol-input-concat-map f1 (funcall g1 x))))) 64 65(defun hol-input-or (f g) 66 "\x -> F x ++ G x" 67 (lexical-let ((f1 f) (g1 g)) 68 (lambda (x) (append (funcall f1 x) (funcall g1 x))))) 69 70(defun hol-input-nonempty () 71 "Only keep pairs with a non-empty first component." 72 (lambda (x) (if (> (length (car x)) 0) (list x)))) 73 74(defun hol-input-prepend (prefix) 75 "Prepend PREFIX to all key sequences." 76 (lexical-let ((prefix1 prefix)) 77 (lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x)))))) 78 79(defun hol-input-prefix (prefix) 80 "Only keep pairs whose key sequence starts with PREFIX." 81 (lexical-let ((prefix1 prefix)) 82 (lambda (x) 83 (if (equal (substring (car x) 0 (length prefix1)) prefix1) 84 (list x))))) 85 86(defun hol-input-suffix (suffix) 87 "Only keep pairs whose key sequence ends with SUFFIX." 88 (lexical-let ((suffix1 suffix)) 89 (lambda (x) 90 (if (equal (substring (car x) 91 (- (length (car x)) (length suffix1))) 92 suffix1) 93 (list x))))) 94 95(defun hol-input-drop (ss) 96 "Drop pairs matching one of the given key sequences. 97SS should be a list of strings." 98 (lexical-let ((ss1 ss)) 99 (lambda (x) (unless (member (car x) ss1) (list x))))) 100 101(defun hol-input-drop-beginning (n) 102 "Drop N characters from the beginning of each key sequence." 103 (lexical-let ((n1 n)) 104 (lambda (x) `((,(substring (car x) n1) . ,(cdr x)))))) 105 106(defun hol-input-drop-end (n) 107 "Drop N characters from the end of each key sequence." 108 (lexical-let ((n1 n)) 109 (lambda (x) 110 `((,(substring (car x) 0 (- (length (car x)) n1)) . 111 ,(cdr x)))))) 112 113(defun hol-input-drop-prefix (prefix) 114 "Only keep pairs whose key sequence starts with PREFIX. 115This prefix is dropped." 116 (hol-input-compose 117 (hol-input-drop-beginning (length prefix)) 118 (hol-input-prefix prefix))) 119 120(defun hol-input-drop-suffix (suffix) 121 "Only keep pairs whose key sequence ends with SUFFIX. 122This suffix is dropped." 123 (lexical-let ((suffix1 suffix)) 124 (hol-input-compose 125 (hol-input-drop-end (length suffix1)) 126 (hol-input-suffix suffix1)))) 127 128;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 129;; Customization 130 131;; The :set keyword is set to 'hol-input-incorporate-changed-setting 132;; so that the input method gets updated immediately when users 133;; customize it. However, the setup functions cannot be run before all 134;; variables have been defined. Hence the :initialize keyword is set to 135;; 'custom-initialize-default to ensure that the setup is not performed 136;; until hol-input-setup is called at the end of this file. 137 138(defgroup hol-input nil 139 "The Hol input method. 140After tweaking these settings you may want to inspect the resulting 141translations using `hol-input-show-translations'." 142 :group 'hol 143 :group 'leim) 144 145(defcustom hol-input-tweak-all 146 '(hol-input-compose 147 (hol-input-prepend "\\") 148 (hol-input-nonempty)) 149 "An expression yielding a function which can be used to tweak 150all translations before they are included in the input method. 151The resulting function (if non-nil) is applied to every 152\(KEY-SEQUENCE . TRANSLATION) pair and should return a list of such 153pairs. (Note that the translations can be anything accepted by 154`quail-defrule'.) 155 156If you change this setting manually (without using the 157customization buffer) you need to call `hol-input-setup' in 158order for the change to take effect." 159 :group 'hol-input 160 :set 'hol-input-incorporate-changed-setting 161 :initialize 'custom-initialize-default 162 :type 'sexp) 163 164(defcustom hol-input-inherit 165 `(("TeX" . (hol-input-compose 166 (hol-input-drop '("geq" "leq" "bullet" "qed" "par")) 167 (hol-input-or 168 (hol-input-drop-prefix "\\") 169 (hol-input-or 170 (hol-input-compose 171 (hol-input-drop '("^o")) 172 (hol-input-prefix "^")) 173 (hol-input-prefix "_"))))) 174 ) 175 "A list of Quail input methods whose translations should be 176inherited by the Hol input method (with the exception of 177translations corresponding to ASCII characters). 178 179The list consists of pairs (qp . tweak), where qp is the name of 180a Quail package, and tweak is an expression of the same kind as 181`hol-input-tweak-all' which is used to tweak the translation 182pairs of the input method. 183 184The inherited translation pairs are added last, after 185`hol-input-user-translations' and `hol-input-translations'. 186 187If you change this setting manually (without using the 188customization buffer) you need to call `hol-input-setup' in 189order for the change to take effect." 190 :group 'hol-input 191 :set 'hol-input-incorporate-changed-setting 192 :initialize 'custom-initialize-default 193 :type '(repeat (cons (string :tag "Quail package") 194 (sexp :tag "Tweaking function")))) 195 196(defcustom hol-input-translations 197 (let ((max-lisp-eval-depth 2800)) `( 198 199 ;; Negation 200 201 ("not" . ("��")) 202 203 ;; Equality and similar symbols. 204 205 ("eq" . ,(hol-input-to-string-list "=������������������������������������ ���������������������������������������������������������������������������")) 206 ("eqn" . ,(hol-input-to-string-list "������ ��� ��� ������ ��� ��� ")) 207 ("equiv" . ,(hol-input-to-string-list "������")) 208 ("iso" . ,(hol-input-to-string-list "������")) 209 210 ("=n" . ("���")) 211 ("~" . ("���")) ("~n" . ("���")) ("homotopy" . ("���")) 212 ("~~" . ("���")) ("~~n" . ("���")) 213 ("~~~" . ("���")) 214 (":~" . ("���")) 215 ("~-" . ("���")) ("~-n" . ("���")) 216 ("-~" . ("���")) 217 ("~=" . ("���")) ("~=n" . ("���")) 218 ("~~-" . ("���")) 219 ("==" . ("���")) ("==n" . ("���")) 220 ("===" . ("���")) 221 (".=" . ("���")) (".=." . ("���")) 222 (":=" . ("���")) ("=:" . ("���")) 223 ("=o" . ("���")) 224 ("(=" . ("���")) 225 ("and=" . ("���")) ("or=" . ("���")) 226 ("*=" . ("���")) 227 ("t=" . ("���")) 228 ("def=" . ("���")) 229 ("m=" . ("���")) 230 ("?=" . ("���")) 231 232 ("pr" . ("���")) 233 234 ("1" . ("���")) 235 ("2" . ("���")) 236 ("3" . ("���")) 237 ("4" . ("���")) 238 ("5" . ("���")) 239 ("6" . ("���")) 240 ("7" . ("���")) 241 ("8" . ("���")) 242 ("9" . ("���")) 243 ("0" . ("���")) 244 245 ;; Inequality and similar symbols. 246 247 ("leq" . ,(hol-input-to-string-list "���������<������ ������������������ ��������� ���������������������")) 248 ("leqn" . ,(hol-input-to-string-list "��������������� ������ ������������ ������ ������ ���")) 249 ("geq" . ,(hol-input-to-string-list "���������>������ ������������������ ��������� ���������������������")) 250 ("geqn" . ,(hol-input-to-string-list "��������������� ��� ��� ������������ ������ ������ ���")) 251 252 ("<=" . ("���")) (">=" . ("���")) 253 ("<=n" . ("���")) (">=n" . ("���")) 254 ("len" . ("���")) ("gen" . ("���")) 255 ("<n" . ("���")) (">n" . ("���")) 256 ("<~" . ("���")) (">~" . ("���")) 257 ("<~n" . ("���")) (">~n" . ("���")) 258 ("<~nn" . ("���")) (">~nn" . ("���")) 259 260 ("ssub" . ("���")) ("ssup" . ("���")) 261 ("ssubn" . ("���")) ("ssupn" . ("���")) 262 ("sub" . ("���")) ("sup" . ("���")) 263 ("subn" . ("���")) ("supn" . ("���")) 264 ("ssqub" . ("���")) ("ssqup" . ("���")) 265 ("squb" . ("���")) ("squp" . ("���")) 266 ("squbn" . ("���")) ("squpn" . ("���")) 267 268 ;; Set membership etc. 269 270 ("member" . ,(hol-input-to-string-list "������������������������������������������������������������")) 271 ("mem" . ("���")) 272 273 ("inn" . ("���")) 274 ("nin" . ("���")) 275 276 ;; Types 277 278 ("T1" . ("Type���")) 279 ("T2" . ("Type���")) 280 ("T+" . ("Type���")) 281 282 ;; Intersections, unions etc. 283 284 ("intersection" . ,(hol-input-to-string-list "������������������������������ ��� ���")) 285 ("union" . ,(hol-input-to-string-list "������������������������������������������������������������")) 286 287 ("and" . ("���")) ("or" . ("���")) 288 ("And" . ("���")) ("Or" . ("���")) 289 ("i" . ("���")) ("un" . ("���")) ("u+" . ("���")) ("u." . ("���")) 290 ("I" . ("���")) ("Un" . ("���")) ("U+" . ("���")) ("U." . ("���")) 291 ("glb" . ("���")) ("lub" . ("���")) 292 ("Glb" . ("���")) ("Lub" . ("���")) 293 294 ;; Entailment etc. 295 296 ("entails" . ,(hol-input-to-string-list "������������������������������������������")) 297 298 ("|-" . ("���")) ("|-n" . ("���")) 299 ("-|" . ("���")) 300 ("|=" . ("���")) ("|=n" . ("���")) 301 ("||-" . ("���")) ("||-n" . ("���")) 302 ("||=" . ("���")) ("||=n" . ("���")) 303 ("|||-" . ("���")) 304 305 ;; Divisibility, parallelity. 306 307 ("|" . ("���")) ("|n" . ("���")) 308 ("||" . ("���")) ("||n" . ("���")) 309 310 ;; Some symbols from logic and set theory. 311 312 ("all" . ("���")) 313 ("ex" . ("���")) 314 ("exn" . ("���")) 315 ("0" . ("���")) 316 ("empty" . ("���")) 317 ("C" . ("���")) 318 ("powerset" . ("����")) 319 320 ;; Corners, ceilings and floors. 321 322 ("c" . ,(hol-input-to-string-list "������������������������")) 323 ("cu" . ,(hol-input-to-string-list "������ ������ ")) 324 ("cl" . ,(hol-input-to-string-list " ������ ������")) 325 326 ("cul" . ("���")) ("cuL" . ("���")) 327 ("cur" . ("���")) ("cuR" . ("���")) 328 ("cll" . ("���")) ("clL" . ("���")) 329 ("clr" . ("���")) ("clR" . ("���")) 330 331 ;; Various operators/symbols. 332 ("tr" . ,(hol-input-to-string-list "������")) 333 ("trans" . ,(hol-input-to-string-list "������")) 334 ("transport" . ("���")) 335 ("con" . ("���")) 336 ("cdot" . ("���")) 337 ("dot" . ("���")) 338 ("sy" . ("�����")) 339 ("inv" . ("�����")) 340 ("-1" . ("�����" "������")) 341 ("-1e" . ("��������")) 342 ("-1f" . ("��������")) 343 ("-1g" . ("��������")) 344 ("-1h" . ("�������")) 345 ("-1i" . ("��������")) 346 ("-1m" . ("��������")) 347 ("-1o" . ("��������")) 348 ("-1r" . ("�������")) 349 ("-1p" . ("��������")) 350 ("-1s" . ("�������")) 351 ("-1v" . ("��������")) 352 ("-1E" . ("��������")) 353 ("-2" . ("�����" "������")) 354 ("-2o" . ("��������")) 355 ("-3" . ("�����")) 356 ("qed" . ("���")) 357 ("x" . ("��")) 358 ("o" . ("���")) 359 ("comp" . ("���")) 360 ("." . ("���")) 361 ("*" . ("���")) 362 (".+" . ("���")) 363 (".-" . ("���")) 364 (":" . ("���")) 365 ("::" . ("���")) 366 ("::-" . ("���")) 367 ("-:" . ("���")) 368 ("+ " . ("���")) 369 ("surd3" . ("���")) 370 ("surd4" . ("���")) 371 ("increment" . ("���")) 372 ("inf" . ("���")) 373 ("&" . ("���")) 374 ("op" . ("������")) 375 ("opf" . ("���������")) 376 377 ;; Circled operators. 378 379 ("o+" . ("���")) 380 ("o--" . ("���")) 381 ("ox" . ("���")) 382 ("o/" . ("���")) 383 ("o." . ("���")) 384 ("oo" . ("���")) 385 ("o*" . ("���*" "���")) 386 ("o=" . ("���")) 387 ("o-" . ("���")) 388 389 ("O+" . ("���")) 390 ("Ox" . ("���")) 391 ("O." . ("���")) 392 ("O*" . ("���")) 393 394 ;; Boxed operators. 395 396 ("b+" . ("���")) 397 ("b-" . ("���")) 398 ("bx" . ("���")) 399 ("b." . ("���")) 400 401 ;; Various symbols. 402 403 ("integral" . ,(hol-input-to-string-list "���������������������������")) 404 ("angle" . ,(hol-input-to-string-list "���������������")) 405 ("join" . ,(hol-input-to-string-list "���������������������������")) 406 407 ;; Arrows. 408 ("iff" . ("���")) ("imp" . ("���")) 409 ("l" . ,(hol-input-to-string-list "��������������������������������������������������������� ��� ������������������������������������ ")) 410 ("r" . ,(hol-input-to-string-list "������������������������������������������������������������ ��� ������������������������������������������������ ������������������������������������������������������������������������������������������������")) 411 ("u" . ,(hol-input-to-string-list "������������������������������������ ��������� ������������������ ")) 412 ("d" . ,(hol-input-to-string-list "������������������������������������ ������������ ��� ")) 413 ("ud" . ,(hol-input-to-string-list "������ ������ ")) 414 ("lr" . ,(hol-input-to-string-list "������ ������������������������ ")) 415 ("ul" . ,(hol-input-to-string-list "������ ������ ")) 416 ("ur" . ,(hol-input-to-string-list "������ ��������� ")) 417 ("dr" . ,(hol-input-to-string-list "������ ��� ��������� ")) 418 ("dl" . ,(hol-input-to-string-list "������ ")) 419 ("==>" . ("���")) ("nattrans" . ("���")) ("nat_trans" . ("���")) 420 421 ("l-" . ("���")) ("<-" . ("���")) ("l=" . ("���")) 422 ("r-" . ("���")) ("->" . ("���")) ("r=" . ("���")) ("=>" . ("���")) ("functor" . ("���")) 423 ("u-" . ("���")) ("u=" . ("���")) 424 ("d-" . ("���")) ("d=" . ("���")) 425 ("ud-" . ("���")) ("ud=" . ("���")) 426 ("lr-" . ("���")) ("<->" . ("���")) ("lr=" . ("���")) ("<=>" . ("���")) 427 ("ul-" . ("���")) ("ul=" . ("���")) 428 ("ur-" . ("���")) ("ur=" . ("���")) 429 ("dr-" . ("���")) ("dr=" . ("���")) 430 ("dl-" . ("���")) ("dl=" . ("���")) 431 432 ("l==" . ("���")) ("l-2" . ("���")) ("l-r-" . ("���")) 433 ("r==" . ("���")) ("r-2" . ("���")) ("r-3" . ("���")) ("r-l-" . ("���")) 434 ("u==" . ("���")) ("u-2" . ("���")) ("u-d-" . ("���")) 435 ("d==" . ("���")) ("d-2" . ("���")) ("d-u-" . ("���")) 436 437 ("l--" . ("���")) ("<--" . ("���")) ("l~" . ("���" "���")) 438 ("r--" . ("���")) ("-->" . ("���")) ("r~" . ("���" "���" "���")) ("hom" . ("���")) 439 ("lr--" . ("���")) ("<-->" . ("���")) ("lr~" . ("���")) 440 441 ("l-n" . ("���")) ("<-n" . ("���")) ("l=n" . ("���")) 442 ("r-n" . ("���")) ("->n" . ("���")) ("r=n" . ("���")) ("=>n" . ("���")) 443 ("lr-n" . ("���")) ("<->n" . ("���")) ("lr=n" . ("���")) ("<=>n" . ("���")) 444 445 ("l-|" . ("���")) ("ll-" . ("���")) 446 ("r-|" . ("���")) ("rr-" . ("���")) 447 ("u-|" . ("���")) ("uu-" . ("���")) 448 ("d-|" . ("���")) ("dd-" . ("���")) 449 ("ud-|" . ("���")) 450 451 ("l->" . ("���")) 452 ("r->" . ("���")) 453 454 ("r-o" . ("���")) ("-o" . ("���")) 455 456 ("dz" . ("���")) 457 458 ;; Ellipsis. 459 460 ("..." . ,(hol-input-to-string-list "������������")) 461 462 ;; Box-drawing characters. 463 464 ("---" . ,(hol-input-to-string-list "������������������������������������������������������������������")) 465 ("--=" . ,(hol-input-to-string-list "��������������������������������� ��������������������������� ���������������������������")) 466 ("--_" . ,(hol-input-to-string-list "��������������������������������������������� 467 ������������������������������������������������������������������������������������������ 468 ������������������������������������������������ ������������")) 469 ("--." . ,(hol-input-to-string-list "������������������ 470 ������������������")) 471 472 ;; Triangles. 473 474 ;; Big/small, black/white. 475 476 ("t" . ,(hol-input-to-string-list "������������������������������������������������������������")) 477 ("Tr" . ,(hol-input-to-string-list "���������������������������������")) 478 479 ("tb" . ,(hol-input-to-string-list "������������������������������")) 480 ("tw" . ,(hol-input-to-string-list "������������������������������")) 481 482 ("Tb" . ,(hol-input-to-string-list "������������")) 483 ("Tw" . ,(hol-input-to-string-list "������������")) 484 485 ;; Squares. 486 487 ("sq" . ,(hol-input-to-string-list "���������������������������������������������������������������������")) 488 ("sqb" . ,(hol-input-to-string-list "���������")) 489 ("sqw" . ,(hol-input-to-string-list "���������")) 490 ("sq." . ("���")) 491 ("sqo" . ("���")) 492 493 ;; Rectangles. 494 495 ("re" . ,(hol-input-to-string-list "������������")) 496 ("reb" . ,(hol-input-to-string-list "������")) 497 ("rew" . ,(hol-input-to-string-list "������")) 498 499 ;; Parallelograms. 500 501 ("pa" . ,(hol-input-to-string-list "������")) 502 ("pab" . ("���")) 503 ("paw" . ("���")) 504 505 ;; Diamonds. 506 507 ("di" . ,(hol-input-to-string-list "���������")) 508 ("dib" . ("���")) 509 ("diw" . ("���")) 510 ("di." . ("���")) 511 512 ;; Circles. 513 514 ("ci" . ,(hol-input-to-string-list "������������������������������������������������������������������������")) 515 ("cib" . ("���")) 516 ("ciw" . ("���")) 517 ("ci." . ("���")) 518 ("ci.." . ("���")) 519 ("ciO" . ("���")) 520 521 ;; Stars. 522 523 ("st" . ,(hol-input-to-string-list "������������������ ���������������������������")) 524 ("st4" . ,(hol-input-to-string-list "������")) 525 ("st6" . ("���")) 526 ("st8" . ("���")) 527 ("st12" . ("���")) 528 529 ;; Blackboard bold letters. 530 531 ("bn" . ("���")) 532 ("bz" . ("���")) 533 ("bq" . ("���")) 534 ("br" . ("���")) 535 ("bc" . ("���")) 536 ("bp" . ("���")) 537 ("bb" . ("����")) 538 ("bsum" . ("���")) 539 540 ;; Blackboard bold numbers. 541 542 ("b0" . ("����")) 543 ("b1" . ("����")) 544 ("b2" . ("����")) 545 ("b3" . ("����")) 546 ("b4" . ("����")) 547 ("b5" . ("����")) 548 ("b6" . ("����")) 549 ("b7" . ("����")) 550 ("b8" . ("����")) 551 ("b9" . ("����")) 552 553 ;; Parentheses. 554 555 ("(" . ,(hol-input-to-string-list "([{�����������������������������������������������������������������������������������������������������������")) 556 (")" . ,(hol-input-to-string-list ")]}�����������������������������������������������������������������������������������������������������������")) 557 558 ("[[" . ("���")) 559 ("]]" . ("���")) 560 ("<" . ("���")) 561 (">" . ("���")) 562 ("<<" . ("���")) 563 (">>" . ("���")) 564 ("f<" . ("���")) 565 ("f>" . ("���")) 566 ("f<<" . ("��")) 567 ("f>>" . ("��")) 568 ("{{" . ("���")) 569 ("}}" . ("���")) 570 571 ("(b" . ("���")) 572 (")b" . ("���")) 573 574 ("lbag" . ("���")) 575 ("rbag" . ("���")) 576 577 ;; lambda 578 579 ("fun" . ("��")) 580 ("lam" . ("��")) 581 582 ("X" . ("���")) 583 584 ;; Primes. 585 586 ("'" . ,(hol-input-to-string-list "������������")) 587 ("`" . ,(hol-input-to-string-list "���������")) 588 589 ;; Fractions. 590 591 ("frac" . ,(hol-input-to-string-list "���������������������������������������������")) 592 593 ;; Bullets. 594 595 ("bu" . ,(hol-input-to-string-list "���������������")) 596 ("bub" . ("���")) 597 ("buw" . ("���")) 598 ("but" . ("���")) 599 600 ;; Types 601 ("nat" . ("���")) 602 ("Nat" . ("���")) 603 ("N" . ("���")) 604 ("N-2" . ("���������")) 605 ("N-1" . ("���������")) 606 ("int" . ("���")) 607 ("Int" . ("���")) 608 ("Z" . ("���")) 609 ("rat" . ("���")) 610 ("Rat" . ("���")) 611 ("Q" . ("���")) 612 ("real" . ("���")) 613 ("Real" . ("���")) 614 ("R" . ("���")) 615 ("Com" . ("���")) 616 ("com" . ("���")) 617 ("C" . ("���")) 618 ("A" . ("����")) 619 ("F" . ("����")) 620 ("H" . ("���")) 621 ("K" . ("����")) 622 623 ("a" . ("��")) 624 ("b" . ("��")) 625 ("g" . ("��")) 626 627 ;; Musical symbols. 628 629 ("note" . ,(hol-input-to-string-list "������������")) 630 ("flat" . ("���")) 631 ("#" . ("���")) 632 633 ;; Other punctuation and symbols. 634 635 ("\\" . ("\\\\")) 636 ("en" . ("���")) 637 ("em" . ("���")) 638 ("^i" . ("���")) 639 ("^o" . ("���")) 640 ("!!" . ("���")) 641 ("??" . ("���")) 642 ("?!" . ("���" "���")) 643 ("!?" . ("���")) 644 ("die" . ,(hol-input-to-string-list "������������������")) 645 ("asterisk" . ,(hol-input-to-string-list "������������������������������������������������������")) 646 ("8<" . ("���" "���")) 647 ("tie" . ("���")) 648 ("undertie" . ("���")) 649 ("apl" . ,(hol-input-to-string-list "��������������������������������������������������������� 650 ��������������������������������������������������������� 651 ��������������������������������������������������������� 652 ���������������������������������������")) 653 654 ;; Some combining characters. 655 ;; 656 ;; The following combining characters also have (other) 657 ;; translations: 658 ;; �� �� �� �� �� �� �� �� �� �� �� �� �� 659 660 ("^--" . ,(hol-input-to-string-list"����")) 661 ("_--" . ,(hol-input-to-string-list"����")) 662 ("^~" . ,(hol-input-to-string-list"����")) 663 ("_~" . ( "��")) 664 ("^." . ,(hol-input-to-string-list"����������")) 665 ("_." . ,(hol-input-to-string-list"����")) 666 ("^l" . ,(hol-input-to-string-list"���������")) 667 ("^l-" . ( "���")) 668 ("^r" . ,(hol-input-to-string-list"���������")) 669 ("^r-" . ( "���")) 670 ("^lr" . ( "���")) 671 ("_lr" . ( "��")) 672 ("^^" . ,(hol-input-to-string-list"������")) 673 ("_^" . ,(hol-input-to-string-list"������")) 674 ("^v" . ,(hol-input-to-string-list"����")) 675 ("_v" . ,(hol-input-to-string-list"������")) 676 677 ;; Shorter forms of many greek letters plus ��. 678 679 ("Ga" . ("��")) ("GA" . ("��")) 680 ("Gb" . ("��")) ("GB" . ("��")) 681 ("Gg" . ("��")) ("GG" . ("��")) 682 ("Gd" . ("��")) ("GD" . ("��")) 683 ("Ge" . ("��")) ("GE" . ("��")) ("eps" . ("��")) 684 ("Gz" . ("��")) ("GZ" . ("��")) 685 ;; \eta \Eta 686 ("Gth" . ("��")) ("GTH" . ("��")) ("th" . ("��")) 687 ("Gi" . ("��")) ("GI" . ("��")) 688 ("Gk" . ("��")) ("GK" . ("��")) 689 ("Gl" . ("��")) ("GL" . ("��")) ("Gl-" . ("��")) 690 ("Gm" . ("��")) ("GM" . ("��")) 691 ("Gn" . ("��")) ("GN" . ("��")) 692 ("Gx" . ("��")) ("GX" . ("��")) 693 ;; \omicron \Omicron 694 ;; \pi \Pi 695 ("Gr" . ("��")) ("GR" . ("��")) 696 ("Gs" . ("��")) ("GS" . ("��")) 697 ("Gt" . ("��")) ("GT" . ("��")) 698 ("Gu" . ("��")) ("GU" . ("��")) 699 ("Gf" . ("��")) ("GF" . ("��")) 700 ("Gc" . ("��")) ("GC" . ("��")) 701 ("Gp" . ("��")) ("GP" . ("��")) 702 ("Go" . ("��")) ("GO" . ("��")) 703 ;; even shorter versions for central type constructors 704 ("S" . ("��")) ("P" . ("��")) 705 706 ;; Mathematical characters 707 708 ("MiA" . ("����")) 709 ("MiB" . ("����")) 710 ("MiC" . ("����")) 711 ("MiD" . ("����")) 712 ("MiE" . ("����")) 713 ("MiF" . ("����")) 714 ("MiG" . ("����")) 715 ("MiH" . ("����")) 716 ("MiI" . ("����")) 717 ("MiJ" . ("����")) 718 ("MiK" . ("����")) 719 ("MiL" . ("����")) 720 ("MiM" . ("����")) 721 ("MiN" . ("����")) 722 ("MiO" . ("����")) 723 ("MiP" . ("����")) 724 ("MiQ" . ("����")) 725 ("MiR" . ("����")) 726 ("MiS" . ("����")) 727 ("MiT" . ("����")) 728 ("MiU" . ("����")) 729 ("MiV" . ("����")) 730 ("MiW" . ("����")) 731 ("MiX" . ("����")) 732 ("MiY" . ("����")) 733 ("MiZ" . ("����")) 734 ("Mia" . ("����")) 735 ("Mib" . ("����")) 736 ("Mic" . ("����")) 737 ("Mid" . ("����")) 738 ("Mie" . ("����")) 739 ("Mif" . ("����")) 740 ("Mig" . ("����")) 741 ("Mii" . ("����")) 742 ("Mij" . ("����")) 743 ("Mik" . ("����")) 744 ("Mil" . ("����")) 745 ("Mim" . ("����")) 746 ("Min" . ("����")) 747 ("Mio" . ("����")) 748 ("Mip" . ("����")) 749 ("Miq" . ("����")) 750 ("Mir" . ("����")) 751 ("Mis" . ("����")) 752 ("Mit" . ("����")) 753 ("Miu" . ("����")) 754 ("Miv" . ("����")) 755 ("Miw" . ("����")) 756 ("Mix" . ("����")) 757 ("Miy" . ("����")) 758 ("Miz" . ("����")) 759 ("MIA" . ("����")) 760 ("MIB" . ("����")) 761 ("MIC" . ("����")) 762 ("MID" . ("����")) 763 ("MIE" . ("����")) 764 ("MIF" . ("����")) 765 ("MIG" . ("����")) 766 ("MIH" . ("����")) 767 ("MII" . ("����")) 768 ("MIJ" . ("����")) 769 ("MIK" . ("����")) 770 ("MIL" . ("����")) 771 ("MIM" . ("����")) 772 ("MIN" . ("����")) 773 ("MIO" . ("����")) 774 ("MIP" . ("����")) 775 ("MIQ" . ("����")) 776 ("MIR" . ("����")) 777 ("MIS" . ("����")) 778 ("MIT" . ("����")) 779 ("MIU" . ("����")) 780 ("MIV" . ("����")) 781 ("MIW" . ("����")) 782 ("MIX" . ("����")) 783 ("MIY" . ("����")) 784 ("MIZ" . ("����")) 785 ("MIa" . ("����")) 786 ("MIb" . ("����")) 787 ("MIc" . ("����")) 788 ("MId" . ("����")) 789 ("MIe" . ("����")) 790 ("MIf" . ("����")) 791 ("MIg" . ("����")) 792 ("MIh" . ("����")) 793 ("MIi" . ("����")) 794 ("MIj" . ("����")) 795 ("MIk" . ("����")) 796 ("MIl" . ("����")) 797 ("MIm" . ("����")) 798 ("MIn" . ("����")) 799 ("MIo" . ("����")) 800 ("MIp" . ("����")) 801 ("MIq" . ("����")) 802 ("MIr" . ("����")) 803 ("MIs" . ("����")) 804 ("MIt" . ("����")) 805 ("MIu" . ("����")) 806 ("MIv" . ("����")) 807 ("MIw" . ("����")) 808 ("MIx" . ("����")) 809 ("MIy" . ("����")) 810 ("MIz" . ("����")) 811 ("McA" . ("����")) 812 ("McC" . ("����")) 813 ("McD" . ("����")) 814 ("McG" . ("����")) 815 ("McJ" . ("����")) 816 ("McK" . ("����")) 817 ("McN" . ("����")) 818 ("McO" . ("����")) 819 ("McP" . ("����")) 820 ("McQ" . ("����")) 821 ("McS" . ("����")) 822 ("McT" . ("����")) 823 ("McU" . ("����")) 824 ("McV" . ("����")) 825 ("McW" . ("����")) 826 ("McX" . ("����")) 827 ("McY" . ("����")) 828 ("McZ" . ("����")) 829 ("Mca" . ("����")) 830 ("Mcb" . ("����")) 831 ("Mcc" . ("����")) 832 ("Mcd" . ("����")) 833 ("Mcf" . ("����")) 834 ("Mch" . ("����")) 835 ("Mci" . ("����")) 836 ("Mcj" . ("����")) 837 ("Mck" . ("����")) 838 ("Mcl" . ("����")) 839 ("Mcm" . ("����")) 840 ("Mcn" . ("����")) 841 ("Mcp" . ("����")) 842 ("Mcq" . ("����")) 843 ("Mcr" . ("����")) 844 ("Mcs" . ("����")) 845 ("Mct" . ("����")) 846 ("Mcu" . ("����")) 847 ("Mcv" . ("����")) 848 ("Mcw" . ("����")) 849 ("Mcx" . ("����")) 850 ("Mcy" . ("����")) 851 ("Mcz" . ("����")) 852 ("MCA" . ("����")) 853 ("MCB" . ("����")) 854 ("MCC" . ("����")) 855 ("MCD" . ("����")) 856 ("MCE" . ("����")) 857 ("MCF" . ("����")) 858 ("MCG" . ("����")) 859 ("MCH" . ("����")) 860 ("MCI" . ("����")) 861 ("MCJ" . ("����")) 862 ("MCK" . ("����")) 863 ("MCL" . ("����")) 864 ("MCM" . ("����")) 865 ("MCN" . ("����")) 866 ("MCO" . ("����")) 867 ("MCP" . ("����")) 868 ("MCQ" . ("����")) 869 ("MCR" . ("����")) 870 ("MCS" . ("����")) 871 ("MCT" . ("����")) 872 ("MCU" . ("����")) 873 ("MCV" . ("����")) 874 ("MCW" . ("����")) 875 ("MCX" . ("����")) 876 ("MCY" . ("����")) 877 ("MCZ" . ("����")) 878 ("MCa" . ("����")) 879 ("MCb" . ("����")) 880 ("MCc" . ("����")) 881 ("MCd" . ("����")) 882 ("MCe" . ("����")) 883 ("MCf" . ("����")) 884 ("MCg" . ("����")) 885 ("MCh" . ("����")) 886 ("MCi" . ("����")) 887 ("MCj" . ("����")) 888 ("MCk" . ("����")) 889 ("MCl" . ("����")) 890 ("MCm" . ("����")) 891 ("MCn" . ("����")) 892 ("MCo" . ("����")) 893 ("MCp" . ("����")) 894 ("MCq" . ("����")) 895 ("MCr" . ("����")) 896 ("MCs" . ("����")) 897 ("MCt" . ("����")) 898 ("MCu" . ("����")) 899 ("MCv" . ("����")) 900 ("MCw" . ("����")) 901 ("MCx" . ("����")) 902 ("MCy" . ("����")) 903 ("MCz" . ("����")) 904 ("MfA" . ("����")) 905 ("MfB" . ("����")) 906 ("MfD" . ("����")) 907 ("MfE" . ("����")) 908 ("MfF" . ("����")) 909 ("MfG" . ("����")) 910 ("MfJ" . ("����")) 911 ("MfK" . ("����")) 912 ("MfL" . ("����")) 913 ("MfM" . ("����")) 914 ("MfN" . ("����")) 915 ("MfO" . ("����")) 916 ("MfP" . ("����")) 917 ("MfQ" . ("����")) 918 ("MfS" . ("����")) 919 ("MfT" . ("����")) 920 ("MfU" . ("����")) 921 ("MfV" . ("����")) 922 ("MfW" . ("����")) 923 ("MfX" . ("����")) 924 ("MfY" . ("����")) 925 ("Mfa" . ("����")) 926 ("Mfb" . ("����")) 927 ("Mfc" . ("����")) 928 ("Mfd" . ("����")) 929 ("Mfe" . ("����")) 930 ("Mff" . ("����")) 931 ("Mfg" . ("����")) 932 ("Mfh" . ("����")) 933 ("Mfi" . ("����")) 934 ("Mfj" . ("����")) 935 ("Mfk" . ("����")) 936 ("Mfl" . ("����")) 937 ("Mfm" . ("����")) 938 ("Mfn" . ("����")) 939 ("Mfo" . ("����")) 940 ("Mfp" . ("����")) 941 ("Mfq" . ("����")) 942 ("Mfr" . ("����")) 943 ("Mfs" . ("����")) 944 ("Mft" . ("����")) 945 ("Mfu" . ("����")) 946 ("Mfv" . ("����")) 947 ("Mfw" . ("����")) 948 ("Mfx" . ("����")) 949 ("Mfy" . ("����")) 950 ("Mfz" . ("����")) 951 952 ;; Some ISO8859-1 characters. 953 954 (" " . (" ")) 955 ("!" . ("��")) 956 ("cent" . ("��")) 957 ("brokenbar" . ("��")) 958 ("degree" . ("��")) 959 ("?" . ("��")) 960 ("^a_" . ("��")) 961 ("^o_" . ("��")) 962 963 ;; Circled, parenthesised etc. numbers and letters. 964 965 ( "(0)" . ,(hol-input-to-string-list " ���")) 966 ( "(1)" . ,(hol-input-to-string-list "������������������")) 967 ( "(2)" . ,(hol-input-to-string-list "������������������")) 968 ( "(3)" . ,(hol-input-to-string-list "������������������")) 969 ( "(4)" . ,(hol-input-to-string-list "������������������")) 970 ( "(5)" . ,(hol-input-to-string-list "������������������")) 971 ( "(6)" . ,(hol-input-to-string-list "������������������")) 972 ( "(7)" . ,(hol-input-to-string-list "������������������")) 973 ( "(8)" . ,(hol-input-to-string-list "������������������")) 974 ( "(9)" . ,(hol-input-to-string-list "������������������")) 975 ("(10)" . ,(hol-input-to-string-list "������������������")) 976 ("(11)" . ,(hol-input-to-string-list "���������")) 977 ("(12)" . ,(hol-input-to-string-list "���������")) 978 ("(13)" . ,(hol-input-to-string-list "���������")) 979 ("(14)" . ,(hol-input-to-string-list "���������")) 980 ("(15)" . ,(hol-input-to-string-list "���������")) 981 ("(16)" . ,(hol-input-to-string-list "���������")) 982 ("(17)" . ,(hol-input-to-string-list "���������")) 983 ("(18)" . ,(hol-input-to-string-list "���������")) 984 ("(19)" . ,(hol-input-to-string-list "���������")) 985 ("(20)" . ,(hol-input-to-string-list "���������")) 986 987 ("(a)" . ,(hol-input-to-string-list "���������")) 988 ("(b)" . ,(hol-input-to-string-list "���������")) 989 ("(c)" . ,(hol-input-to-string-list "���������")) 990 ("(d)" . ,(hol-input-to-string-list "���������")) 991 ("(e)" . ,(hol-input-to-string-list "���������")) 992 ("(f)" . ,(hol-input-to-string-list "���������")) 993 ("(g)" . ,(hol-input-to-string-list "���������")) 994 ("(h)" . ,(hol-input-to-string-list "���������")) 995 ("(i)" . ,(hol-input-to-string-list "���������")) 996 ("(j)" . ,(hol-input-to-string-list "���������")) 997 ("(k)" . ,(hol-input-to-string-list "���������")) 998 ("(l)" . ,(hol-input-to-string-list "���������")) 999 ("(m)" . ,(hol-input-to-string-list "���������")) 1000 ("(n)" . ,(hol-input-to-string-list "���������")) 1001 ("(o)" . ,(hol-input-to-string-list "���������")) 1002 ("(p)" . ,(hol-input-to-string-list "���������")) 1003 ("(q)" . ,(hol-input-to-string-list "���������")) 1004 ("(r)" . ,(hol-input-to-string-list "���������")) 1005 ("(s)" . ,(hol-input-to-string-list "���������")) 1006 ("(t)" . ,(hol-input-to-string-list "���������")) 1007 ("(u)" . ,(hol-input-to-string-list "���������")) 1008 ("(v)" . ,(hol-input-to-string-list "���������")) 1009 ("(w)" . ,(hol-input-to-string-list "���������")) 1010 ("(x)" . ,(hol-input-to-string-list "���������")) 1011 ("(y)" . ,(hol-input-to-string-list "���������")) 1012 ("(z)" . ,(hol-input-to-string-list "���������")) 1013 ("y" . ("��")) 1014 1015 1016 )) 1017 "A list of translations specific to the Hol input method. 1018Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). 1019All the translation strings are possible translations 1020of the given key sequence; if there is more than one you can choose 1021between them using the arrow keys. 1022 1023Note that if you customize this setting you will not 1024automatically benefit (or suffer) from modifications to its 1025default value when the library is updated. If you just want to 1026add some bindings it is probably a better idea to customize 1027`hol-input-user-translations'. 1028 1029These translation pairs are included after those in 1030`hol-input-user-translations', but before the ones inherited 1031from other input methods (see `hol-input-inherit'). 1032 1033If you change this setting manually (without using the 1034customization buffer) you need to call `hol-input-setup' in 1035order for the change to take effect." 1036 :group 'hol-input 1037 :set 'hol-input-incorporate-changed-setting 1038 :initialize 'custom-initialize-default 1039 :type '(repeat (cons (string :tag "Key sequence") 1040 (repeat :tag "Translations" string)))) 1041 1042(defcustom hol-input-user-translations nil 1043 "Like `hol-input-translations', but more suitable for user 1044customizations since by default it is empty. 1045 1046These translation pairs are included first, before those in 1047`hol-input-translations' and the ones inherited from other input 1048methods." 1049 :group 'hol-input 1050 :set 'hol-input-incorporate-changed-setting 1051 :initialize 'custom-initialize-default 1052 :type '(repeat (cons (string :tag "Key sequence") 1053 (repeat :tag "Translations" string)))) 1054 1055;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1056;; Inspecting and modifying translation maps 1057 1058(defun hol-input-get-translations (qp) 1059 "Return a list containing all translations from the Quail 1060package QP (except for those corresponding to ASCII). 1061Each pair in the list has the form (KEY-SEQUENCE . TRANSLATION)." 1062 (with-temp-buffer 1063 (activate-input-method qp) ; To make sure that the package is loaded. 1064 (unless (quail-package qp) 1065 (error "%s is not a Quail package." qp)) 1066 (let ((decode-map (list 'decode-map))) 1067 (quail-build-decode-map (list (quail-map)) "" decode-map 0) 1068 (cdr decode-map)))) 1069 1070(defun hol-input-show-translations (qp) 1071 "Display all translations used by the Quail package QP (a string). 1072\(Except for those corresponding to ASCII)." 1073 (interactive (list (read-input-method-name 1074 "Quail input method (default %s): " "Hol"))) 1075 (let ((buf (concat "*" qp " input method translations*"))) 1076 (with-output-to-temp-buffer buf 1077 (with-current-buffer buf 1078 (quail-insert-decode-map 1079 (cons 'decode-map (hol-input-get-translations qp))))))) 1080 1081(defun hol-input-add-translations (trans) 1082 "Add the given translations TRANS to the Hol input method. 1083TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The 1084translations are appended to the current translations." 1085 (with-temp-buffer 1086 (dolist (tr (hol-input-concat-map (eval hol-input-tweak-all) trans)) 1087 (quail-defrule (car tr) (cdr tr) "Hol" t)))) 1088 1089(defun hol-input-inherit-package (qp &optional fun) 1090 "Let the Hol input method inherit the translations from the 1091Quail package QP (except for those corresponding to ASCII). 1092 1093The optional function FUN can be used to modify the translations. 1094It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return 1095a list of such pairs." 1096 (let ((trans (hol-input-get-translations qp))) 1097 (hol-input-add-translations 1098 (if fun (hol-input-concat-map fun trans) 1099 trans)))) 1100 1101;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1102;; Setting up the input method 1103 1104(defun hol-input-setup () 1105 "Set up the Hol input method based on the customisable 1106variables and underlying input methods." 1107 1108 ;; Create (or reset) the input method. 1109 (with-temp-buffer 1110 (quail-define-package "Hol" "UTF-8" "���" t ; guidance 1111 "Hol input method. 1112The purpose of this input method is to edit Hol programs, but 1113since it is highly customisable it can be made useful for other 1114tasks as well." 1115 nil nil nil nil nil nil t ; maximum-shortest 1116 )) 1117 1118 (hol-input-add-translations 1119 (mapcar (lambda (tr) (cons (car tr) (vconcat (cdr tr)))) 1120 (append hol-input-user-translations 1121 hol-input-translations))) 1122 (dolist (def hol-input-inherit) 1123 (hol-input-inherit-package (car def) 1124 (eval (cdr def))))) 1125 1126(defun hol-input-incorporate-changed-setting (sym val) 1127 "Update the Hol input method based on the customisable 1128variables and underlying input methods. 1129Suitable for use in the :set field of `defcustom'." 1130 (set-default sym val) 1131 (hol-input-setup)) 1132 1133;; Set up the input method. 1134 1135(hol-input-setup) 1136(quail-defrule "/\\" "���" "Hol") 1137(quail-defrule "\\/" "���" "Hol") 1138(quail-defrule "==>" "���" "Hol") 1139(quail-defrule "!" "���" "Hol") 1140(quail-defrule "?" "���" "Hol") 1141(quail-defrule "?!" ["���!"] "Hol") 1142(quail-defrule "!!" "!" "Hol") 1143(quail-defrule "??" "?" "Hol") 1144(quail-defrule "<=>" "���" "Hol") 1145(quail-defrule "<>" "���" "Hol") 1146(quail-defrule "<=" "���" "Hol") 1147 1148;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1149;; Administrative details 1150 1151(provide 'hol-input) 1152;;; hol-input.el ends here 1153