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