equal
deleted
inserted
replaced
54 |
54 |
55 /* snapshot and rendering */ |
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 |
58 |
59 def rendering(options: Options): VSCode_Rendering = |
59 def rendering(options: Options, text_length: Length): VSCode_Rendering = |
60 new VSCode_Rendering(this, snapshot(), options, session.resources) |
60 new VSCode_Rendering(this, snapshot(), options, text_length, session.resources) |
61 } |
61 } |