diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2008-01-27 14:51:05 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-27 14:51:05 +0000 |
commit | 84b0f643c1085907e8da1897d0562cea8941481f (patch) | |
tree | 5705d2a45b596cb4749b75474c6bcea50a6110b4 | |
parent | e675749f2e881639096f0a05f161ea4bdc0afbdb (diff) |
Switch token table mapping destination from glyph names to unicode strings. Generate from Isabelle.sym
-rw-r--r-- | isar/isar-unicode-tokens.el | 389 |
1 files changed, 287 insertions, 102 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index e03ae0d3..0564d28f 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -1,4 +1,5 @@ -;;; isar-unicode-tokens.el --- Tokens for Unicode Tokens package +;;; -*- coding: utf-8; -*- +;; isar-unicode-tokens.el --- Tokens for Unicode Tokens package ;; ;; Copyright(C) 2008 David Aspinall / LFCS Edinburgh ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> @@ -16,107 +17,291 @@ (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"))) - - + '(; token name, unicode char sequence + ("alpha" . "α") + ("beta" . "β") + ("gamma" . "γ") + ("delta" . "δ") + ("epsilon" . "ϵ") + ("varepsilon" . "ε") + ("zeta" . "ζ") + ("eta" . "η") + ("theta" . "θ") + ("vartheta" . "ϑ") + ("iota" . "ι") + ("kappa" . "κ") + ("lambda" . "λ") + ("mu" . "μ") + ("nu" . "ν") + ("xi" . "ξ") + ("o" . "ο") + ("pi" . "π") + ("varpi" . "ϖ") + ("rho" . "ρ") + ("varrho" . "ϱ") + ("sigma" . "σ") + ("varsigma" . "ς") + ("tau" . "τ") + ("upsilon" . "υ") + ("phi" . "ϕ") + ("varphi" . "φ") + ("chi" . "χ") + ("psi" . "ψ") + ("omega" . "ω") + ("Gamma" . "Γ") + ("Delta" . "Δ") + ("Theta" . "Θ") + ("Lambda" . "Λ") + ("Xi" . "Ξ") + ("Pi" . "Π") + ("Sigma" . "Σ") + ("Upsilon" . "Υ") + ("Phi" . "Φ") + ("Psi" . "Ψ") + ("Omega" . "Ω") + ("aleph" . "ℵ") + ("hbar" . "ℏ") + ("index" . "ı") + ("ell" . "ℓ") + ("wp" . "℘") + ("Re" . "ℜ") + ("Im" . "ℑ") + ("partial" . "∂") + ("infinity" . "∞") + ("Box" . "□") + ("emptyset" . "∅") + ("nabla" . "∇") + ("surd" . "√") + ("top" . "⊤") + ("angle" . "∠") + ("triangle" . "△") + ("Diamond" . "◇") + ("exists" . "∃") + ("forall" . "∀") + ("not" . "¬") + ("flat" . "♭") + ("natural" . "♮") + ("sharp" . "♯") + ("clubsuit" . "♣") + ("diamondsuit" . "♢") + ("heartsuit" . "♡") + ("spadesuit" . "♠") + ("Sum" . "∑") + ("Prod" . "∏") + ("Coprod" . "∐") + ("integral" . "∫") + ("ointegral" . "∮") + ("Inter" . "⋂") + ("Union" . "⋃") + ("Squnion" . "⨆") + ("Or" . "⋁") + ("And" . "⋀") + ("Odot" . "⨀") + ("Otimes" . "⨂") + ("Oplus" . "⨁") + ("Uplus" . "⨄") + ("pm" . "±") + ("mp" . "∓") + ("setminus" . "∖") + ("cdot" . "⋅") + ("times" . "×") + ("ast" . "∗") + ("star" . "⋆") + ("diamond" . "⋄") + ("circ" . "∘") + ("bullet" . "∙") + ("div" . "÷") + ("lhd" . "⊲") + ("inter" . "∩") + ("union" . "∪") + ("uplus" . "⊎") + ("sqinter" . "⊓") + ("squnion" . "⊔") + ("triangleleft" . "◁") + ("triangleright" . "▷") + ("wr" . "≀") + ("bigcirc" . "◯") + ("bigtriangleup" . "△") + ("bigtriangledown" . "▽") + ("rhd" . "⊳") + ("or" . "∨") + ("and" . "∧") + ("oplus" . "⊕") + ("ominus" . "⊖") + ("otimes" . "⊗") + ("oslash" . "⊘") + ("odot" . "⊙") + ("dagger" . "†") + ("ddagger" . "‡") + ("amalg" . "⨿") + ("unlhd" . "⊴") + ("unrhd" . "⊵") + ("le" . "≤") + ("prec" . "≺") + ("preceq" . "≼") + ("lless" . "≪") + ("subset" . "⊂") + ("subseteq" . "⊆") + ("sqsubseteq" . "⊑") + ("in" . "∈") + ("turnstile" . "⊢") + ("smile" . "⌣") + ("frown" . "⌢") + ("sqsubset" . "⊏") + ("ge" . "≥") + ("succ" . "≻") + ("succeq" . "≽") + ("ggreater" . "≫") + ("supset" . "⊃") + ("supseteq" . "⊇") + ("sqsupseteq" . "⊒") + ("ni" . "∋") + ("dashv" . "⊣") + ("mid" . "∣") + ("parallel" . "∥") + ("sqsupset" . "⊐") + ("equiv" . "≡") + ("sim" . "∼") + ("simeq" . "≃") + ("asymp" . "≍") + ("approx" . "≈") + ("cong" . "≅") + ("bowtie" . "⋈") + ("propto" . "∝") + ("Turnstile" . "⊨") + ("doteq" . "≐") + ("bottom" . "⊥") + ("Join" . "⨝") + ("notlt" . "≮") + ("notle" . "≰") + ("notprec" . "⊀") + ("notpreceq" . "⋠") + ("notsubset" . "⊄") + ("notsubseteq" . "⊈") + ("not" . "⋢") + ("notgt" . "≯") + ("notge" . "≱") + ("notsucc" . "⊁") + ("notsucceq" . "⋡") + ("notsupset" . "⊅") + ("notsupseteq" . "⊉") + ("notsqsupseteq" . "⋣") + ("noteq" . "≠") + ("notequiv" . "≢") + ("notsim" . "≁") + ("notsimeq" . "≄") + ("notapprox" . "≉") + ("notcong" . "≇") + ("notasymp" . "≭") + ("leftarrow" . "←") + ("Leftarrow" . "⇐") + ("rightarrow" . "→") + ("Rightarrow" . "⇒") + ("leftrightarrow" . "↔") + ("Leftrightarrow" . "⇔") + ("mapsto" . "↦") + ("hookleftarrow" . "↩") + ("leftharpoonup" . "↼") + ("leftharpoondown" . "↽") + ("rightleftharpoons" . "⇌") +;; Real long symbols: + ("longleftarrow" . "⟵") + ("Longleftarrow" . "⟸") + ("longrightarrow" . "⟶") + ("Longrightarrow" . "⟹") + ("longleftrightarrow" . "⟷") + ("longmapsto" . "⟼") +;; Faked long symbols (older Linux versions): +;;; ("longleftarrow" . "←=") +;;; ("Longleftarrow" . "⇐=") +;;; ("longrightarrow" . "=→") +;;; ("Longrightarrow" . "=⇒") +;;; ("longleftrightarrow" . "←→") +;;; ("Longleftrightarrow" . "⇐⇒") +;;; ("longmapsto" . "❘→") + ("hookrightarrow" . "↪") + ("rightharpoonup" . "⇀") + ("rightharpoondown" . "⇁") + ("leadsto" . "↝") + ("uparrow" . "↑") + ("Uparrow" . "⇑") + ("downarrow" . "↓") + ("Downarrow" . "⇓") + ("updown" . "↕") + ("Updownarrow" . "⇕") + ("nearrow" . "↗") + ("searrow" . "↘") + ("swarrow" . "↙") + ("nwarrow" . "↖") + ("lfloor" . "⌊") + ("langle" . "⟨") + ("lceil" . "⌈") + ("langle" . "⟪") + ("lbrakk" . "⟦") + ("rfloor" . "⌋") + ("rangle" . "⟩") + ("rceil" . "⌉") + ("rangle" . "⟫") + ("rbrakk" . "⟧") + ("vdots" . "⋮") + ("cdots" . "⋯") + ("ddots" . "⋱") + ("closequote" . "’") + ("openquote" . "‘") + ("opendblquote" . "”") + ("closedblquote" . "“") + ("hyphen" . "‐") + ("endash" . "–") + ("emdash" . "—") + ("prime" . "′") + ("doubleprime" . "″") + ("tripleprime" . "‴") + ("quadrupleprime" . "⁗") + ("exclamdown" . "¡") + ("questiondown" . "¿") + ("nbspace" . " ") + ("thinspace" . " ") + ("copyright" . "©") + ("pounds" . "£") + ("ldots" . "…") + ("nat" . "ℕ") + ("int" . "ℤ") + ("rat" . "ℚ") + ("real" . "ℝ") + ("complex" . "ℂ") + ("notin" . "∉") + ("Colon" . "∷") + ("bar" . "¦") + ("Sqinter" . "⨅") + ("guillemotleft" . "«") + ("guillemotright" . "»") + ("acute" . "´") + ("inverse" . "¯") + ("notni" . "∌") + ("euro" . "€") + ("yen" . "¥") + ("cent" . "¢") + ;;; Not in plain Isar-X-Symbol + ("oe" . "œ") + ("OE" . "Œ") + ("ae" . "æ") + ("AE" . "Æ") + ("aa" . "å") + ("AA" . "Å") + ("o" . "ø") ;; LaTeX \o + ("O" . "Ø") ;; LaTeX \O + ("l" . "ł") ;; LaTeX \l + ("L" . "Ł") ;; LaTeX \L + ("ss" . "ß") ;; LaTeX \ss + ("S" . "§") ;; LaTeX \S + ("P" . "¶") ;; LaTeX \P + ("colonequals" . "≔") + ("ff" . "ff") + ("fi" . "fi") + ("fl" . "fl") + ("ffi" . "ffi") + ("ffl" . "ffl") + )) (provide 'isar-unicode-tokens) |