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()) }