| changeset 64649 | d67c3094a0c2 |
| parent 64622 | 529bbb8977c7 |
| child 64667 | cdb0d559a24b |
--- a/src/Tools/VSCode/src/document_model.scala Wed Dec 21 21:18:37 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Dec 21 22:27:38 2016 +0100 @@ -57,5 +57,5 @@ def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) def rendering(options: Options): VSCode_Rendering = - new VSCode_Rendering(snapshot(), options, session.resources) + new VSCode_Rendering(this, snapshot(), options, session.resources) }