src/Tools/VSCode/src/document_model.scala
changeset 65213 51c0f094dc02
parent 65199 6bd7081f8319
child 65359 9ca34f0407a9
--- a/src/Tools/VSCode/src/document_model.scala	Mon Mar 13 17:21:46 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Mar 13 20:33:42 2017 +0100
@@ -167,6 +167,6 @@
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot, resources)
+    new VSCode_Rendering(this, snapshot)
   def rendering(): VSCode_Rendering = rendering(snapshot())
 }