clarified options;

--- a/src/Tools/VSCode/etc/options	Tue Mar 07 00:06:16 2017 +0100
+++ b/src/Tools/VSCode/etc/options	Tue Mar 07 10:52:04 2017 +0100
@@ -18,5 +18,8 @@
 option vscode_timing_threshold : real = 0.1
   -- "default threshold for timing display (seconds)"
 
+option vscode_pide_extensions : bool = false
+  -- "use PIDE extensions for Language Server Protocol"
+
 option vscode_unicode_symbols : bool = false
   -- "output Isabelle symbols via Unicode (according to etc/symbols)"

--- a/src/Tools/VSCode/extension/src/extension.ts	Tue Mar 07 00:06:16 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Mar 07 10:52:04 2017 +0100
@@ -23,7 +23,7 @@
     vscode.window.showErrorMessage("Missing user settings: isabelle.home")
   else {
     let isabelle_tool = isabelle_home.concat("/bin/isabelle")
-    let standard_args = ["-o", "vscode_unicode_symbols"]
+    let standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
     let run =
       is_windows ?
         { command: cygwin_root.concat("/bin/bash"),

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 00:06:16 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 10:52:04 2017 +0100
@@ -71,7 +71,7 @@
         model.content.try_get_text(complete_range) match {
           case Some(original) =>
             names.complete(complete_range, Completion.History.empty,
-                resources.decode_text, original) match {
+                resources.unicode_symbols, original) match {
               case Some(result) =>
                 result.items.map(item =>
                   Protocol.CompletionItem(

--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 07 00:06:16 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 07 10:52:04 2017 +0100
@@ -47,6 +47,14 @@
   private val state = Synchronized(VSCode_Resources.State())
 
 
+  /* options */
+
+  def pide_extensions: Boolean = options.bool("vscode_pide_extensions")
+  def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols")
+  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
+  def message_margin: Int = options.int("vscode_message_margin")
+
+
   /* document node name */
 
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
@@ -238,8 +246,10 @@
           yield {
             for (diags <- changed_diags)
               channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags)))
-            for (decos <- changed_decos; deco <- decos)
-              channel.write(rendering.decoration_output(deco).json(file))
+            if (pide_extensions) {
+              for (decos <- changed_decos; deco <- decos)
+                channel.write(rendering.decoration_output(deco).json(file))
+            }
             (file, model1)
           }
         st.copy(
@@ -252,12 +262,8 @@
 
   /* output text */
 
-  def decode_text: Boolean = options.bool("vscode_unicode_symbols")
-  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
-  def message_margin: Int = options.int("vscode_message_margin")
-
   def output_text(s: String): String =
-    if (decode_text) Symbol.decode(s) else Symbol.encode(s)
+    if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s)
 
   def output_xml(xml: XML.Tree): String =
     output_text(XML.content(xml))