# 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