src/Tools/VSCode/src/document_model.scala
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64707 7157685b71e3
--- 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)
 }