diff options
Diffstat (limited to 'isa/x-symbol-isa.el')
-rw-r--r-- | isa/x-symbol-isa.el | 70 |
1 files changed, 54 insertions, 16 deletions
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el index 2ab3c42a..e724de13 100644 --- a/isa/x-symbol-isa.el +++ b/isa/x-symbol-isa.el @@ -1,11 +1,7 @@ -;; x-symbol-isa.el token language "Isabelle Symbols" for package x-symbol -;; -;; Author: David von Oheimb -;; Copyright 1998 Technische Universitaet Muenchen -;; Maintainer: ?? -;; -;; $Id$ -;; +;; ID: $Id$ +;; Author: David von Oheimb +;; Copyright 1998 Technische Universitaet Muenchen +;;; token language "Isabelle Symbols" for package x-symbol (provide 'x-symbol-isa) (defvar x-symbol-isa-required-fonts nil) @@ -49,7 +45,7 @@ (defvar x-symbol-isa-token-list 'x-symbol-isa-default-token-list) (defvar x-symbol-isa-symbol-table '(;;symbols (isabelle14 font) - (visiblespace () "\\\\<space2>") + (visiblespace () "\\\\<spacespace>") (Gamma () "\\\\<Gamma>") (Delta () "\\\\<Delta>") (Theta () "\\\\<Theta>") @@ -92,8 +88,8 @@ (floorright () "\\\\<rfloor>") (bardash () "\\\\<turnstile>") (bardashdbl () "\\\\<Turnstile>") - (braceleft2 () "\\\\<lbrakk>") ;##missing symbol - (braceright2 () "\\\\<rbrakk>") ;##missing symbol + (semanticsleft () "\\\\<lbrakk>") + (semanticsright () "\\\\<rbrakk>") (periodcentered () "\\\\<cdot>") (element () "\\\\<in>") (reflexsubset () "\\\\<subseteq>") @@ -103,7 +99,7 @@ (bigunion () "\\\\<Union>") (sqintersection () "\\\\<sqinter>") (squnion () "\\\\<squnion>") -; (??????? () "\\\\<Sqinter>") ;##missing symbol + (bigsqintersection () "\\\\<Sqinter>") (bigsqunion () "\\\\<Squnion>") (perpendicular1 () "\\\\<bottom>") (dotequal () "\\\\<doteq>") @@ -118,12 +114,12 @@ (similar () "\\\\<sim>") (simequal () "\\\\<simeq>") (lessequal () "\\\\<le>") - (therefore1 () "\\\\<Colon>") ;##missing symbol + (coloncolon () "\\\\<Colon>") (arrowleft () "\\\\<leftarrow>") (endash () "\\\\<midarrow>") (arrowright () "\\\\<rightarrow>") (arrowdblleft () "\\\\<Leftarrow>") - (rightleftharpoons () "\\\\<Midarrow>") ;##missing symbol (unnecessary) +; (rightleftharpoons () "\\\\<Midarrow>") ;missing symbol (but not necessary) (arrowdblright () "\\\\<Rightarrow>") (frown () "\\\\<bow>") (mapsto () "\\\\<mapsto>") @@ -138,8 +134,8 @@ (circleslash () "\\\\<oslash>") (propersubset () "\\\\<subset>") (infinity () "\\\\<infinity>") - (box () "\\\\<box>") ;##too big - (smllozenge () "\\\\<diamond>") ;##too small + (box () "\\\\<box>") + (lozenge1 () "\\\\<diamond>") (circ () "\\\\<circ>") (bullet () "\\\\<bullet>") (bardbl () "\\\\<parallel>") @@ -147,12 +143,37 @@ (copyright () "\\\\<copyright>") )) (defvar x-symbol-isa-xsymbol-table '(;;xsymbols + (plusminus () "\\\\<plusminus>") + (division () "\\\\<div>") (longarrowright () "\\\\<longrightarrow>") (longarrowleft () "\\\\<longleftarrow>") (longarrowboth () "\\\\<longleftrightarrow>") (longarrowdblright () "\\\\<Longrightarrow>") (longarrowdblleft () "\\\\<Longleftarrow>") (longarrowdblboth () "\\\\<Longleftrightarrow>") + (brokenbar () "\\\\<brokenbar>") + (hyphen () "\\\\<hyphen>") + (macron () "\\\\<macron>") + (exclamdown () "\\\\<exclamdown>") + (questiondown () "\\\\<questiondown>") + (guillemotleft () "\\\\<guillemotleft>") + (guillemotright () "\\\\<guillemotright>") + (degree () "\\\\<degree>") + (onesuperior () "\\\\<onesuperior>") + (onequarter () "\\\\<onequarter>") + (twosuperior () "\\\\<twosuperior>") + (onehalf () "\\\\<onehalf>") + (threesuperior () "\\\\<threesuperior>") + (threequarters () "\\\\<threequarters>") + (paragraph () "\\\\<paragraph>") + (registered () "\\\\<registered>") + (ordfeminine () "\\\\<ordfeminine>") + (ordmasculine () "\\\\<ordmasculine>") + (section () "\\\\<section>") + (pounds () "\\\\<pounds>") + (yen () "\\\\<yen>") + (cent () "\\\\<cent>") + (currency () "\\\\<currency>") )) (defvar x-symbol-isa-user-table nil) (defvar x-symbol-isa-table @@ -182,5 +203,22 @@ +;;;=========================================================================== +;;; useful key bindings +;;;=========================================================================== + +(global-set-key [(meta l)] 'x-symbol-INSERT-lambda) + +(global-set-key [(meta n)] 'x-symbol-INSERT-notsign) +(global-set-key [(meta a)] 'x-symbol-INSERT-logicaland) +(global-set-key [(meta o)] 'x-symbol-INSERT-logicalor) +(global-set-key [(meta f)] 'x-symbol-INSERT-universal1) +(global-set-key [(meta t)] 'x-symbol-INSERT-existential1) +(global-set-key [(meta A)] 'x-symbol-INSERT-biglogicaland) +(global-set-key [(meta e)] 'x-symbol-INSERT-equivalence) +(global-set-key [(meta u)] 'x-symbol-INSERT-notequal) +(global-set-key [(meta m)] 'x-symbol-INSERT-arrowdblright) +(global-set-key [(meta x)] 'x-symbol-INSERT-multiply) +(global-set-key [(meta i)] 'x-symbol-INSERT-longarrowright) |