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 */