src/Tools/VSCode/src/document_model.scala
changeset 64667 cdb0d559a24b
parent 64649 d67c3094a0c2
child 64671 93e375bd3283
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:07:54 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 23 19:19:59 2016 +0100
@@ -56,6 +56,6 @@
 
   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
 
-  def rendering(options: Options): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot(), options, session.resources)
+  def rendering(options: Options, text_length: Length): VSCode_Rendering =
+    new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
 }