# HG changeset patch
# User wenzelm
# Date 1497345214 -7200
# Node ID 9a719681309ebf81609c49bf1e1475a06468fd59
# Parent  1700b74ebbb99365bf64e80d980d812039479a6c
obsolete;

diff -r 1700b74ebbb9 -r 9a719681309e src/Tools/VSCode/extension/isabelle-symbols.json
--- a/src/Tools/VSCode/extension/isabelle-symbols.json	Mon Jun 12 21:14:38 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-{
-  "prettifySymbolsMode.substitutions": [
-      {
-        "language": "isabelle",
-        "revealOn": "none",
-        "adjustCursorMovement": true,
-        "substitutions": [
-          {"ugly":"\\\\\\<zero\\>","pretty":"𝟬"},
-          {"ugly":"\\\\\\<one\\>","pretty":"𝟭"},
-          {"ugly":"\\\\\\<two\\>","pretty":"𝟮"},
-          {"ugly":"\\\\\\<three\\>","pretty":"𝟯"},
-          {"ugly":"\\\\\\<four\\>","pretty":"𝟰"},
-          {"ugly":"\\\\\\<five\\>","pretty":"𝟱"},
-          {"ugly":"\\\\\\<six\\>","pretty":"𝟲"},
-          {"ugly":"\\\\\\<seven\\>","pretty":"𝟳"},
-          {"ugly":"\\\\\\<eight\\>","pretty":"𝟴"},
-          {"ugly":"\\\\\\<nine\\>","pretty":"𝟵"},
-          {"ugly":"\\\\\\<A\\>","pretty":"𝒜"},
-          {"ugly":"\\\\\\<B\\>","pretty":"ℬ"},
-          {"ugly":"\\\\\\<C\\>","pretty":"𝒞"},
-          {"ugly":"\\\\\\<D\\>","pretty":"𝒟"},
-          {"ugly":"\\\\\\<E\\>","pretty":"ℰ"},
-          {"ugly":"\\\\\\<F\\>","pretty":"ℱ"},
-          {"ugly":"\\\\\\<G\\>","pretty":"𝒢"},
-          {"ugly":"\\\\\\<H\\>","pretty":"ℋ"},
-          {"ugly":"\\\\\\<I\\>","pretty":"ℐ"},
-          {"ugly":"\\\\\\<J\\>","pretty":"𝒥"},
-          {"ugly":"\\\\\\<K\\>","pretty":"𝒦"},
-          {"ugly":"\\\\\\<L\\>","pretty":"ℒ"},
-          {"ugly":"\\\\\\<M\\>","pretty":"ℳ"},
-          {"ugly":"\\\\\\<N\\>","pretty":"𝒩"},
-          {"ugly":"\\\\\\<O\\>","pretty":"𝒪"},
-          {"ugly":"\\\\\\<P\\>","pretty":"𝒫"},
-          {"ugly":"\\\\\\<Q\\>","pretty":"𝒬"},
-          {"ugly":"\\\\\\<R\\>","pretty":"ℛ"},
-          {"ugly":"\\\\\\<S\\>","pretty":"𝒮"},
-          {"ugly":"\\\\\\<T\\>","pretty":"𝒯"},
-          {"ugly":"\\\\\\<U\\>","pretty":"𝒰"},
-          {"ugly":"\\\\\\<V\\>","pretty":"𝒱"},
-          {"ugly":"\\\\\\<W\\>","pretty":"𝒲"},
-          {"ugly":"\\\\\\<X\\>","pretty":"𝒳"},
-          {"ugly":"\\\\\\<Y\\>","pretty":"𝒴"},
-          {"ugly":"\\\\\\<Z\\>","pretty":"𝒵"},
-          {"ugly":"\\\\\\<a\\>","pretty":"𝖺"},
-          {"ugly":"\\\\\\<b\\>","pretty":"𝖻"},
-          {"ugly":"\\\\\\<c\\>","pretty":"𝖼"},
-          {"ugly":"\\\\\\<d\\>","pretty":"𝖽"},
-          {"ugly":"\\\\\\<e\\>","pretty":"𝖾"},
-          {"ugly":"\\\\\\<f\\>","pretty":"𝖿"},
-          {"ugly":"\\\\\\<g\\>","pretty":"𝗀"},
-          {"ugly":"\\\\\\<h\\>","pretty":"𝗁"},
-          {"ugly":"\\\\\\<i\\>","pretty":"𝗂"},
-          {"ugly":"\\\\\\<j\\>","pretty":"𝗃"},
-          {"ugly":"\\\\\\<k\\>","pretty":"𝗄"},
-          {"ugly":"\\\\\\<l\\>","pretty":"𝗅"},
-          {"ugly":"\\\\\\<m\\>","pretty":"𝗆"},
-          {"ugly":"\\\\\\<n\\>","pretty":"𝗇"},
-          {"ugly":"\\\\\\<o\\>","pretty":"𝗈"},
-          {"ugly":"\\\\\\<p\\>","pretty":"𝗉"},
-          {"ugly":"\\\\\\<q\\>","pretty":"𝗊"},
-          {"ugly":"\\\\\\<r\\>","pretty":"𝗋"},
-          {"ugly":"\\\\\\<s\\>","pretty":"𝗌"},
-          {"ugly":"\\\\\\<t\\>","pretty":"𝗍"},
-          {"ugly":"\\\\\\<u\\>","pretty":"𝗎"},
-          {"ugly":"\\\\\\<v\\>","pretty":"𝗏"},
-          {"ugly":"\\\\\\<w\\>","pretty":"𝗐"},
-          {"ugly":"\\\\\\<x\\>","pretty":"𝗑"},
-          {"ugly":"\\\\\\<y\\>","pretty":"𝗒"},
-          {"ugly":"\\\\\\<z\\>","pretty":"𝗓"},
-          {"ugly":"\\\\\\<AA\\>","pretty":"𝔄"},
-          {"ugly":"\\\\\\<BB\\>","pretty":"𝔅"},
-          {"ugly":"\\\\\\<CC\\>","pretty":"ℭ"},
-          {"ugly":"\\\\\\<DD\\>","pretty":"𝔇"},
-          {"ugly":"\\\\\\<EE\\>","pretty":"𝔈"},
-          {"ugly":"\\\\\\<FF\\>","pretty":"𝔉"},
-          {"ugly":"\\\\\\<GG\\>","pretty":"𝔊"},
-          {"ugly":"\\\\\\<HH\\>","pretty":"ℌ"},
-          {"ugly":"\\\\\\<II\\>","pretty":"ℑ"},
-          {"ugly":"\\\\\\<JJ\\>","pretty":"𝔍"},
-          {"ugly":"\\\\\\<KK\\>","pretty":"𝔎"},
-          {"ugly":"\\\\\\<LL\\>","pretty":"𝔏"},
-          {"ugly":"\\\\\\<MM\\>","pretty":"𝔐"},
-          {"ugly":"\\\\\\<NN\\>","pretty":"𝔑"},
-          {"ugly":"\\\\\\<OO\\>","pretty":"𝔒"},
-          {"ugly":"\\\\\\<PP\\>","pretty":"𝔓"},
-          {"ugly":"\\\\\\<QQ\\>","pretty":"𝔔"},
-          {"ugly":"\\\\\\<RR\\>","pretty":"ℜ"},
-          {"ugly":"\\\\\\<SS\\>","pretty":"𝔖"},
-          {"ugly":"\\\\\\<TT\\>","pretty":"𝔗"},
-          {"ugly":"\\\\\\<UU\\>","pretty":"𝔘"},
-          {"ugly":"\\\\\\<VV\\>","pretty":"𝔙"},
-          {"ugly":"\\\\\\<WW\\>","pretty":"𝔚"},
-          {"ugly":"\\\\\\<XX\\>","pretty":"𝔛"},
-          {"ugly":"\\\\\\<YY\\>","pretty":"𝔜"},
-          {"ugly":"\\\\\\<ZZ\\>","pretty":"ℨ"},
-          {"ugly":"\\\\\\<aa\\>","pretty":"𝔞"},
-          {"ugly":"\\\\\\<bb\\>","pretty":"𝔟"},
-          {"ugly":"\\\\\\<cc\\>","pretty":"𝔠"},
-          {"ugly":"\\\\\\<dd\\>","pretty":"𝔡"},
-          {"ugly":"\\\\\\<ee\\>","pretty":"𝔢"},
-          {"ugly":"\\\\\\<ff\\>","pretty":"𝔣"},
-          {"ugly":"\\\\\\<gg\\>","pretty":"𝔤"},
-          {"ugly":"\\\\\\<hh\\>","pretty":"𝔥"},
-          {"ugly":"\\\\\\<ii\\>","pretty":"𝔦"},
-          {"ugly":"\\\\\\<jj\\>","pretty":"𝔧"},
-          {"ugly":"\\\\\\<kk\\>","pretty":"𝔨"},
-          {"ugly":"\\\\\\<ll\\>","pretty":"𝔩"},
-          {"ugly":"\\\\\\<mm\\>","pretty":"𝔪"},
-          {"ugly":"\\\\\\<nn\\>","pretty":"𝔫"},
-          {"ugly":"\\\\\\<oo\\>","pretty":"𝔬"},
-          {"ugly":"\\\\\\<pp\\>","pretty":"𝔭"},
-          {"ugly":"\\\\\\<qq\\>","pretty":"𝔮"},
-          {"ugly":"\\\\\\<rr\\>","pretty":"𝔯"},
-          {"ugly":"\\\\\\<ss\\>","pretty":"𝔰"},
-          {"ugly":"\\\\\\<tt\\>","pretty":"𝔱"},
-          {"ugly":"\\\\\\<uu\\>","pretty":"𝔲"},
-          {"ugly":"\\\\\\<vv\\>","pretty":"𝔳"},
-          {"ugly":"\\\\\\<ww\\>","pretty":"𝔴"},
-          {"ugly":"\\\\\\<xx\\>","pretty":"𝔵"},
-          {"ugly":"\\\\\\<yy\\>","pretty":"𝔶"},
-          {"ugly":"\\\\\\<zz\\>","pretty":"𝔷"},
-          {"ugly":"\\\\\\<alpha\\>","pretty":"α"},
-          {"ugly":"\\\\\\<beta\\>","pretty":"β"},
-          {"ugly":"\\\\\\<gamma\\>","pretty":"γ"},
-          {"ugly":"\\\\\\<delta\\>","pretty":"δ"},
-          {"ugly":"\\\\\\<epsilon\\>","pretty":"ε"},
-          {"ugly":"\\\\\\<zeta\\>","pretty":"ζ"},
-          {"ugly":"\\\\\\<eta\\>","pretty":"η"},
-          {"ugly":"\\\\\\<theta\\>","pretty":"θ"},
-          {"ugly":"\\\\\\<iota\\>","pretty":"ι"},
-          {"ugly":"\\\\\\<kappa\\>","pretty":"κ"},
-          {"ugly":"\\\\\\<lambda\\>","pretty":"λ"},
-          {"ugly":"\\\\\\<mu\\>","pretty":"μ"},
-          {"ugly":"\\\\\\<nu\\>","pretty":"ν"},
-          {"ugly":"\\\\\\<xi\\>","pretty":"ξ"},
-          {"ugly":"\\\\\\<pi\\>","pretty":"π"},
-          {"ugly":"\\\\\\<rho\\>","pretty":"ρ"},
-          {"ugly":"\\\\\\<sigma\\>","pretty":"σ"},
-          {"ugly":"\\\\\\<tau\\>","pretty":"τ"},
-          {"ugly":"\\\\\\<upsilon\\>","pretty":"υ"},
-          {"ugly":"\\\\\\<phi\\>","pretty":"φ"},
-          {"ugly":"\\\\\\<chi\\>","pretty":"χ"},
-          {"ugly":"\\\\\\<psi\\>","pretty":"ψ"},
-          {"ugly":"\\\\\\<omega\\>","pretty":"ω"},
-          {"ugly":"\\\\\\<Gamma\\>","pretty":"Γ"},
-          {"ugly":"\\\\\\<Delta\\>","pretty":"Δ"},
-          {"ugly":"\\\\\\<Theta\\>","pretty":"Θ"},
-          {"ugly":"\\\\\\<Lambda\\>","pretty":"Λ"},
-          {"ugly":"\\\\\\<Xi\\>","pretty":"Ξ"},
-          {"ugly":"\\\\\\<Pi\\>","pretty":"Π"},
-          {"ugly":"\\\\\\<Sigma\\>","pretty":"Σ"},
-          {"ugly":"\\\\\\<Upsilon\\>","pretty":"Υ"},
-          {"ugly":"\\\\\\<Phi\\>","pretty":"Φ"},
-          {"ugly":"\\\\\\<Psi\\>","pretty":"Ψ"},
-          {"ugly":"\\\\\\<Omega\\>","pretty":"Ω"},
-          {"ugly":"\\\\\\<bool\\>","pretty":"𝔹"},
-          {"ugly":"\\\\\\<complex\\>","pretty":"ℂ"},
-          {"ugly":"\\\\\\<nat\\>","pretty":"ℕ"},
-          {"ugly":"\\\\\\<rat\\>","pretty":"ℚ"},
-          {"ugly":"\\\\\\<real\\>","pretty":"ℝ"},
-          {"ugly":"\\\\\\<int\\>","pretty":"ℤ"},
-          {"ugly":"\\\\\\<leftarrow\\>","pretty":"←"},
-          {"ugly":"\\\\\\<longleftarrow\\>","pretty":"⟵"},
-          {"ugly":"\\\\\\<longlongleftarrow\\>","pretty":"⤎"},
-          {"ugly":"\\\\\\<longlonglongleftarrow\\>","pretty":"⇠"},
-          {"ugly":"\\\\\\<rightarrow\\>","pretty":"→"},
-          {"ugly":"\\\\\\<longrightarrow\\>","pretty":"⟶"},
-          {"ugly":"\\\\\\<longlongrightarrow\\>","pretty":"⤏"},
-          {"ugly":"\\\\\\<longlonglongrightarrow\\>","pretty":"⇢"},
-          {"ugly":"\\\\\\<Leftarrow\\>","pretty":"⇐"},
-          {"ugly":"\\\\\\<Longleftarrow\\>","pretty":"⟸"},
-          {"ugly":"\\\\\\<Lleftarrow\\>","pretty":"⇚"},
-          {"ugly":"\\\\\\<Rightarrow\\>","pretty":"⇒"},
-          {"ugly":"\\\\\\<Longrightarrow\\>","pretty":"⟹"},
-          {"ugly":"\\\\\\<Rrightarrow\\>","pretty":"⇛"},
-          {"ugly":"\\\\\\<leftrightarrow\\>","pretty":"↔"},
-          {"ugly":"\\\\\\<longleftrightarrow\\>","pretty":"⟷"},
-          {"ugly":"\\\\\\<Leftrightarrow\\>","pretty":"⇔"},
-          {"ugly":"\\\\\\<Longleftrightarrow\\>","pretty":"⟺"},
-          {"ugly":"\\\\\\<mapsto\\>","pretty":"↦"},
-          {"ugly":"\\\\\\<longmapsto\\>","pretty":"⟼"},
-          {"ugly":"\\\\\\<midarrow\\>","pretty":"─"},
-          {"ugly":"\\\\\\<Midarrow\\>","pretty":"═"},
-          {"ugly":"\\\\\\<hookleftarrow\\>","pretty":"↩"},
-          {"ugly":"\\\\\\<hookrightarrow\\>","pretty":"↪"},
-          {"ugly":"\\\\\\<leftharpoondown\\>","pretty":"↽"},
-          {"ugly":"\\\\\\<rightharpoondown\\>","pretty":"⇁"},
-          {"ugly":"\\\\\\<leftharpoonup\\>","pretty":"↼"},
-          {"ugly":"\\\\\\<rightharpoonup\\>","pretty":"⇀"},
-          {"ugly":"\\\\\\<rightleftharpoons\\>","pretty":"⇌"},
-          {"ugly":"\\\\\\<leadsto\\>","pretty":"↝"},
-          {"ugly":"\\\\\\<downharpoonleft\\>","pretty":"⇃"},
-          {"ugly":"\\\\\\<downharpoonright\\>","pretty":"⇂"},
-          {"ugly":"\\\\\\<upharpoonleft\\>","pretty":"↿"},
-          {"ugly":"\\\\\\<restriction\\>","pretty":"↾"},
-          {"ugly":"\\\\\\<Colon\\>","pretty":"∷"},
-          {"ugly":"\\\\\\<up\\>","pretty":"↑"},
-          {"ugly":"\\\\\\<Up\\>","pretty":"⇑"},
-          {"ugly":"\\\\\\<down\\>","pretty":"↓"},
-          {"ugly":"\\\\\\<Down\\>","pretty":"⇓"},
-          {"ugly":"\\\\\\<updown\\>","pretty":"↕"},
-          {"ugly":"\\\\\\<Updown\\>","pretty":"⇕"},
-          {"ugly":"\\\\\\<langle\\>","pretty":"⟨"},
-          {"ugly":"\\\\\\<rangle\\>","pretty":"⟩"},
-          {"ugly":"\\\\\\<lceil\\>","pretty":"⌈"},
-          {"ugly":"\\\\\\<rceil\\>","pretty":"⌉"},
-          {"ugly":"\\\\\\<lfloor\\>","pretty":"⌊"},
-          {"ugly":"\\\\\\<rfloor\\>","pretty":"⌋"},
-          {"ugly":"\\\\\\<lparr\\>","pretty":"⦇"},
-          {"ugly":"\\\\\\<rparr\\>","pretty":"⦈"},
-          {"ugly":"\\\\\\<lbrakk\\>","pretty":"⟦"},
-          {"ugly":"\\\\\\<rbrakk\\>","pretty":"⟧"},
-          {"ugly":"\\\\\\<lbrace\\>","pretty":"⦃"},
-          {"ugly":"\\\\\\<rbrace\\>","pretty":"⦄"},
-          {"ugly":"\\\\\\<guillemotleft\\>","pretty":"«"},
-          {"ugly":"\\\\\\<guillemotright\\>","pretty":"»"},
-          {"ugly":"\\\\\\<bottom\\>","pretty":"⊥"},
-          {"ugly":"\\\\\\<top\\>","pretty":"⊤"},
-          {"ugly":"\\\\\\<and\\>","pretty":"∧"},
-          {"ugly":"\\\\\\<And\\>","pretty":"⋀"},
-          {"ugly":"\\\\\\<or\\>","pretty":"∨"},
-          {"ugly":"\\\\\\<Or\\>","pretty":"⋁"},
-          {"ugly":"\\\\\\<forall\\>","pretty":"∀"},
-          {"ugly":"\\\\\\<exists\\>","pretty":"∃"},
-          {"ugly":"\\\\\\<nexists\\>","pretty":"∄"},
-          {"ugly":"\\\\\\<not\\>","pretty":"¬"},
-          {"ugly":"\\\\\\<circle\\>","pretty":"○"},
-          {"ugly":"\\\\\\<box\\>","pretty":"□"},
-          {"ugly":"\\\\\\<diamond\\>","pretty":"◇"},
-          {"ugly":"\\\\\\<diamondop\\>","pretty":"⋄"},
-          {"ugly":"\\\\\\<turnstile\\>","pretty":"⊢"},
-          {"ugly":"\\\\\\<Turnstile\\>","pretty":"⊨"},
-          {"ugly":"\\\\\\<tturnstile\\>","pretty":"⊩"},
-          {"ugly":"\\\\\\<TTurnstile\\>","pretty":"⊫"},
-          {"ugly":"\\\\\\<stileturn\\>","pretty":"⊣"},
-          {"ugly":"\\\\\\<surd\\>","pretty":"√"},
-          {"ugly":"\\\\\\<le\\>","pretty":"≤"},
-          {"ugly":"\\\\\\<ge\\>","pretty":"≥"},
-          {"ugly":"\\\\\\<lless\\>","pretty":"≪"},
-          {"ugly":"\\\\\\<ggreater\\>","pretty":"≫"},
-          {"ugly":"\\\\\\<lesssim\\>","pretty":"≲"},
-          {"ugly":"\\\\\\<greatersim\\>","pretty":"≳"},
-          {"ugly":"\\\\\\<lessapprox\\>","pretty":"⪅"},
-          {"ugly":"\\\\\\<greaterapprox\\>","pretty":"⪆"},
-          {"ugly":"\\\\\\<in\\>","pretty":"∈"},
-          {"ugly":"\\\\\\<notin\\>","pretty":"∉"},
-          {"ugly":"\\\\\\<subset\\>","pretty":"⊂"},
-          {"ugly":"\\\\\\<supset\\>","pretty":"⊃"},
-          {"ugly":"\\\\\\<subseteq\\>","pretty":"⊆"},
-          {"ugly":"\\\\\\<supseteq\\>","pretty":"⊇"},
-          {"ugly":"\\\\\\<sqsubset\\>","pretty":"⊏"},
-          {"ugly":"\\\\\\<sqsupset\\>","pretty":"⊐"},
-          {"ugly":"\\\\\\<sqsubseteq\\>","pretty":"⊑"},
-          {"ugly":"\\\\\\<sqsupseteq\\>","pretty":"⊒"},
-          {"ugly":"\\\\\\<inter\\>","pretty":"∩"},
-          {"ugly":"\\\\\\<Inter\\>","pretty":"⋂"},
-          {"ugly":"\\\\\\<union\\>","pretty":"∪"},
-          {"ugly":"\\\\\\<Union\\>","pretty":"⋃"},
-          {"ugly":"\\\\\\<squnion\\>","pretty":"⊔"},
-          {"ugly":"\\\\\\<Squnion\\>","pretty":"⨆"},
-          {"ugly":"\\\\\\<sqinter\\>","pretty":"⊓"},
-          {"ugly":"\\\\\\<Sqinter\\>","pretty":"⨅"},
-          {"ugly":"\\\\\\<setminus\\>","pretty":"∖"},
-          {"ugly":"\\\\\\<propto\\>","pretty":"∝"},
-          {"ugly":"\\\\\\<uplus\\>","pretty":"⊎"},
-          {"ugly":"\\\\\\<Uplus\\>","pretty":"⨄"},
-          {"ugly":"\\\\\\<noteq\\>","pretty":"≠"},
-          {"ugly":"\\\\\\<sim\\>","pretty":"∼"},
-          {"ugly":"\\\\\\<doteq\\>","pretty":"≐"},
-          {"ugly":"\\\\\\<simeq\\>","pretty":"≃"},
-          {"ugly":"\\\\\\<approx\\>","pretty":"≈"},
-          {"ugly":"\\\\\\<asymp\\>","pretty":"≍"},
-          {"ugly":"\\\\\\<cong\\>","pretty":"≅"},
-          {"ugly":"\\\\\\<smile\\>","pretty":"⌣"},
-          {"ugly":"\\\\\\<equiv\\>","pretty":"≡"},
-          {"ugly":"\\\\\\<frown\\>","pretty":"⌢"},
-          {"ugly":"\\\\\\<Join\\>","pretty":"⋈"},
-          {"ugly":"\\\\\\<bowtie\\>","pretty":"⨝"},
-          {"ugly":"\\\\\\<prec\\>","pretty":"≺"},
-          {"ugly":"\\\\\\<succ\\>","pretty":"≻"},
-          {"ugly":"\\\\\\<preceq\\>","pretty":"≼"},
-          {"ugly":"\\\\\\<succeq\\>","pretty":"≽"},
-          {"ugly":"\\\\\\<parallel\\>","pretty":"∥"},
-          {"ugly":"\\\\\\<bar\\>","pretty":"¦"},
-          {"ugly":"\\\\\\<plusminus\\>","pretty":"±"},
-          {"ugly":"\\\\\\<minusplus\\>","pretty":"∓"},
-          {"ugly":"\\\\\\<times\\>","pretty":"×"},
-          {"ugly":"\\\\\\<div\\>","pretty":"÷"},
-          {"ugly":"\\\\\\<cdot\\>","pretty":"⋅"},
-          {"ugly":"\\\\\\<star\\>","pretty":"⋆"},
-          {"ugly":"\\\\\\<bullet\\>","pretty":"∙"},
-          {"ugly":"\\\\\\<circ\\>","pretty":"∘"},
-          {"ugly":"\\\\\\<dagger\\>","pretty":"†"},
-          {"ugly":"\\\\\\<ddagger\\>","pretty":"‡"},
-          {"ugly":"\\\\\\<lhd\\>","pretty":"⊲"},
-          {"ugly":"\\\\\\<rhd\\>","pretty":"⊳"},
-          {"ugly":"\\\\\\<unlhd\\>","pretty":"⊴"},
-          {"ugly":"\\\\\\<unrhd\\>","pretty":"⊵"},
-          {"ugly":"\\\\\\<triangleleft\\>","pretty":"◃"},
-          {"ugly":"\\\\\\<triangleright\\>","pretty":"▹"},
-          {"ugly":"\\\\\\<triangle\\>","pretty":"△"},
-          {"ugly":"\\\\\\<triangleq\\>","pretty":"≜"},
-          {"ugly":"\\\\\\<oplus\\>","pretty":"⊕"},
-          {"ugly":"\\\\\\<Oplus\\>","pretty":"⨁"},
-          {"ugly":"\\\\\\<otimes\\>","pretty":"⊗"},
-          {"ugly":"\\\\\\<Otimes\\>","pretty":"⨂"},
-          {"ugly":"\\\\\\<odot\\>","pretty":"⊙"},
-          {"ugly":"\\\\\\<Odot\\>","pretty":"⨀"},
-          {"ugly":"\\\\\\<ominus\\>","pretty":"⊖"},
-          {"ugly":"\\\\\\<oslash\\>","pretty":"⊘"},
-          {"ugly":"\\\\\\<dots\\>","pretty":"…"},
-          {"ugly":"\\\\\\<cdots\\>","pretty":"⋯"},
-          {"ugly":"\\\\\\<Sum\\>","pretty":"∑"},
-          {"ugly":"\\\\\\<Prod\\>","pretty":"∏"},
-          {"ugly":"\\\\\\<Coprod\\>","pretty":"∐"},
-          {"ugly":"\\\\\\<infinity\\>","pretty":"∞"},
-          {"ugly":"\\\\\\<integral\\>","pretty":"∫"},
-          {"ugly":"\\\\\\<ointegral\\>","pretty":"∮"},
-          {"ugly":"\\\\\\<clubsuit\\>","pretty":"♣"},
-          {"ugly":"\\\\\\<diamondsuit\\>","pretty":"♢"},
-          {"ugly":"\\\\\\<heartsuit\\>","pretty":"♡"},
-          {"ugly":"\\\\\\<spadesuit\\>","pretty":"♠"},
-          {"ugly":"\\\\\\<aleph\\>","pretty":"ℵ"},
-          {"ugly":"\\\\\\<emptyset\\>","pretty":"∅"},
-          {"ugly":"\\\\\\<nabla\\>","pretty":"∇"},
-          {"ugly":"\\\\\\<partial\\>","pretty":"∂"},
-          {"ugly":"\\\\\\<flat\\>","pretty":"♭"},
-          {"ugly":"\\\\\\<natural\\>","pretty":"♮"},
-          {"ugly":"\\\\\\<sharp\\>","pretty":"♯"},
-          {"ugly":"\\\\\\<angle\\>","pretty":"∠"},
-          {"ugly":"\\\\\\<copyright\\>","pretty":"©"},
-          {"ugly":"\\\\\\<registered\\>","pretty":"®"},
-          {"ugly":"\\\\\\<hyphen\\>","pretty":"­"},
-          {"ugly":"\\\\\\<inverse\\>","pretty":"¯"},
-          {"ugly":"\\\\\\<onequarter\\>","pretty":"¼"},
-          {"ugly":"\\\\\\<onehalf\\>","pretty":"½"},
-          {"ugly":"\\\\\\<threequarters\\>","pretty":"¾"},
-          {"ugly":"\\\\\\<ordfeminine\\>","pretty":"ª"},
-          {"ugly":"\\\\\\<ordmasculine\\>","pretty":"º"},
-          {"ugly":"\\\\\\<section\\>","pretty":"§"},
-          {"ugly":"\\\\\\<paragraph\\>","pretty":"¶"},
-          {"ugly":"\\\\\\<exclamdown\\>","pretty":"¡"},
-          {"ugly":"\\\\\\<questiondown\\>","pretty":"¿"},
-          {"ugly":"\\\\\\<euro\\>","pretty":"€"},
-          {"ugly":"\\\\\\<pounds\\>","pretty":"£"},
-          {"ugly":"\\\\\\<yen\\>","pretty":"¥"},
-          {"ugly":"\\\\\\<cent\\>","pretty":"¢"},
-          {"ugly":"\\\\\\<currency\\>","pretty":"¤"},
-          {"ugly":"\\\\\\<degree\\>","pretty":"°"},
-          {"ugly":"\\\\\\<amalg\\>","pretty":"⨿"},
-          {"ugly":"\\\\\\<mho\\>","pretty":"℧"},
-          {"ugly":"\\\\\\<lozenge\\>","pretty":"◊"},
-          {"ugly":"\\\\\\<wp\\>","pretty":"℘"},
-          {"ugly":"\\\\\\<wrong\\>","pretty":"≀"},
-          {"ugly":"\\\\\\<acute\\>","pretty":"´"},
-          {"ugly":"\\\\\\<index\\>","pretty":"ı"},
-          {"ugly":"\\\\\\<dieresis\\>","pretty":"¨"},
-          {"ugly":"\\\\\\<cedilla\\>","pretty":"¸"},
-          {"ugly":"\\\\\\<hungarumlaut\\>","pretty":"˝"},
-          {"ugly":"\\\\\\<bind\\>","pretty":"⤜"},
-          {"ugly":"\\\\\\<then\\>","pretty":"⪢"},
-          {"ugly":"\\\\\\<some\\>","pretty":"ϵ"},
-          {"ugly":"\\\\\\<hole\\>","pretty":"⌑"},
-          {"ugly":"\\\\\\<newline\\>","pretty":"⏎"},
-          {"ugly":"\\\\\\<comment\\>","pretty":"―"},
-          {"ugly":"\\\\\\<open\\>","pretty":"‹"},
-          {"ugly":"\\\\\\<close\\>","pretty":"›"},
-          {"ugly":"\\\\\\<\\^here\\>","pretty":"⌂"},
-          {"ugly":"\\\\\\<\\^undefined\\>","pretty":"❖"},
-          {"ugly":"\\\\\\<\\^noindent\\>","pretty":"⇤"},
-          {"ugly":"\\\\\\<\\^smallskip\\>","pretty":"┈"},
-          {"ugly":"\\\\\\<\\^medskip\\>","pretty":"┉"},
-          {"ugly":"\\\\\\<\\^bigskip\\>","pretty":"━"},
-          {"ugly":"\\\\\\<\\^item\\>","pretty":"▪"},
-          {"ugly":"\\\\\\<\\^enum\\>","pretty":"▸"},
-          {"ugly":"\\\\\\<\\^descr\\>","pretty":"➧"},
-          {"ugly":"\\\\\\<\\^footnote\\>","pretty":"⁋"},
-          {"ugly":"\\\\\\<\\^verbatim\\>","pretty":"▩"},
-          {"ugly":"\\\\\\<\\^theory_text\\>","pretty":"⬚"},
-          {"ugly":"\\\\\\<\\^emph\\>","pretty":"∗"},
-          {"ugly":"\\\\\\<\\^bold\\>","pretty":"❙"},
-          {"ugly":"\\\\\\<\\^sub\\>","pretty":"⇩"},
-          {"ugly":"\\\\\\<\\^sup\\>","pretty":"⇧"},
-          {"ugly":"\\\\\\<\\^bsub\\>","pretty":"⇘"},
-          {"ugly":"\\\\\\<\\^esub\\>","pretty":"⇙"},
-          {"ugly":"\\\\\\<\\^bsup\\>","pretty":"⇗"},
-          {"ugly":"\\\\\\<\\^esup\\>","pretty":"⇖"},
-          {"ugly":"\\\\\\<\\^file\\>","pretty":"🗏"},
-          {"ugly":"\\\\\\<\\^dir\\>","pretty":"🗀"},
-          {"ugly":"\\\\\\<\\^url\\>","pretty":"🌐"},
-          {"ugly":"\\\\\\<\\^doc\\>","pretty":"📓"},
-          {"ugly":"\\\\\\<\\^action\\>","pretty":"☛"}]
-      }
-    ]
-}
\ No newline at end of file