# HG changeset patch
# User wenzelm
# Date 1483045829 -3600
# Node ID 08c2d80428ff7922599e4f209f43a0989ab2e851
# Parent  a115391494edf92b712014a611c8ef307f62832f
re-use options from resources;

diff -r a115391494ed -r 08c2d80428ff src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Dec 29 21:54:04 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Dec 29 22:10:29 2016 +0100
@@ -72,6 +72,5 @@
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
-  def rendering(options: Options): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot(), options, resources)
+  def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
 }
diff -r a115391494ed -r 08c2d80428ff src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Dec 29 21:54:04 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Dec 29 22:10:29 2016 +0100
@@ -101,7 +101,7 @@
   def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
     for {
       model <- resources.get_model(node_pos.name)
-      rendering = model.rendering(options)
+      rendering = model.rendering()
       offset <- model.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
diff -r a115391494ed -r 08c2d80428ff src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Thu Dec 29 21:54:04 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Thu Dec 29 22:10:29 2016 +0100
@@ -37,9 +37,8 @@
 class VSCode_Rendering(
     val model: Document_Model,
     snapshot: Document.Snapshot,
-    options: Options,
     resources: VSCode_Resources)
-  extends Rendering(snapshot, options, resources)
+  extends Rendering(snapshot, resources.options, resources)
 {
   /* diagnostics */
 
diff -r a115391494ed -r 08c2d80428ff src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 29 21:54:04 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 29 22:10:29 2016 +0100
@@ -101,7 +101,7 @@
           for {
             node_name <- st.pending_output.iterator
             model <- st.models.get(node_name.node)
-            rendering = model.rendering(options)
+            rendering = model.rendering()
             (diagnostics, model1) <- model.publish_diagnostics(rendering)
           } yield {
             channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))