src/Tools/VSCode/src/document_model.scala
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64707 7157685b71e3
equal deleted inserted replaced
64703:a115391494ed 64704:08c2d80428ff
    70 
    70 
    71   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
    71   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
    72 
    72 
    73   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    73   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    74 
    74 
    75   def rendering(options: Options): VSCode_Rendering =
    75   def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
    76     new VSCode_Rendering(this, snapshot(), options, resources)
       
    77 }
    76 }