diff -r f6c6e25ef782 -r cdb0d559a24b src/Tools/VSCode/src/document_model.scala --- 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) }