src/Tools/VSCode/src/document_model.scala
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
child 64649 d67c3094a0c2
equal deleted inserted replaced
64621:7116f2634e32 64622:529bbb8977c7
    50     else Nil
    50     else Nil
    51 
    51 
    52   def unchanged: Document_Model = if (changed) copy(changed = false) else this
    52   def unchanged: Document_Model = if (changed) copy(changed = false) else this
    53 
    53 
    54 
    54 
    55   /* snapshot */
    55   /* snapshot and rendering */
    56 
    56 
    57   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    57   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
       
    58 
       
    59   def rendering(options: Options): VSCode_Rendering =
       
    60     new VSCode_Rendering(snapshot(), options, session.resources)
    58 }
    61 }