# HG changeset patch
# User wenzelm
# Date 1484146879 -3600
# Node ID 9c194386db8db360bc2dbdeea3393282c84e3e80
# Parent  2d594dabcca653e70e301b8ec9adde11848613b5
generated configuration for Prettify Symbols Mode;

diff -r 2d594dabcca6 -r 9c194386db8d src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Wed Jan 11 14:48:07 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Wed Jan 11 16:01:19 2017 +0100
@@ -115,7 +115,8 @@
       Update_Then.isabelle_tool,
       Update_Theorems.isabelle_tool,
       isabelle.vscode.Grammar.isabelle_tool,
-      isabelle.vscode.Server.isabelle_tool)
+      isabelle.vscode.Server.isabelle_tool,
+      isabelle.vscode.Symbols.isabelle_tool)
 
   private def list_internal(): List[(String, String)] =
     for (tool <- internal_tools.toList if tool.accessible)
diff -r 2d594dabcca6 -r 9c194386db8d src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Jan 11 14:48:07 2017 +0100
+++ b/src/Pure/build-jars	Wed Jan 11 16:01:19 2017 +0100
@@ -163,6 +163,7 @@
   ../Tools/VSCode/src/grammar.scala
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala
+  ../Tools/VSCode/src/symbols.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
 )
diff -r 2d594dabcca6 -r 9c194386db8d src/Tools/VSCode/README.md
--- a/src/Tools/VSCode/README.md	Wed Jan 11 14:48:07 2017 +0100
+++ b/src/Tools/VSCode/README.md	Wed Jan 11 16:01:19 2017 +0100
@@ -29,6 +29,8 @@
 
 * shell> `isabelle vscode_grammar`
 
+* shell> `isabelle vscode_symbols`
+
 * shell> `vsce package`
 
 
diff -r 2d594dabcca6 -r 9c194386db8d src/Tools/VSCode/extension/isabelle-symbols.json
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/isabelle-symbols.json	Wed Jan 11 16:01:19 2017 +0100
@@ -0,0 +1,395 @@
+{
+  "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
diff -r 2d594dabcca6 -r 9c194386db8d src/Tools/VSCode/src/symbols.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/symbols.scala	Wed Jan 11 16:01:19 2017 +0100
@@ -0,0 +1,55 @@
+/*  Title:      Tools/VSCode/src/symbols.scala
+    Author:     Makarius
+
+Generate configuration for VSCode editor extension Prettify Symbols Mode.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Symbols
+{
+  /* generate configuration */
+
+  def prettify_config: String =
+    """{
+  "prettifySymbolsMode.substitutions": [
+      {
+        "language": "isabelle",
+        "revealOn": "none",
+        "adjustCursorMovement": true,
+        "substitutions": [""" +
+          (for ((s, c) <- Symbol.codes)
+           yield
+            JSON.Format(
+              Map("ugly" -> Library.escape_regex(s),
+                "pretty" -> Library.escape_regex(Codepoint.string(c)))))
+            .mkString("\n          ", ",\n          ", "") +
+        """]
+      }
+    ]
+}"""
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool = Isabelle_Tool("vscode_symbols",
+    "generate configuration for VSCode editor extension Prettify Symbols Mode", args =>
+  {
+    val getopts = Getopts("""
+Usage: isabelle vscode_symbols
+
+  Generate configuration for VSCode editor extension Prettify Symbols Mode.
+""")
+
+    val more_args = getopts(args)
+    if (more_args.nonEmpty) getopts.usage()
+
+    val output_path = Path.explode("isabelle-symbols.json")
+    Output.writeln(output_path.implode)
+    File.write_backup(output_path, prettify_config)
+  })
+}