--- a/src/Tools/VSCode/src/vscode_model.scala Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Fri Dec 23 22:41:47 2022 +0100
@@ -78,6 +78,7 @@
) extends Document.Model {
model =>
+
/* content */
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -106,7 +107,7 @@
caret: Option[Line.Position]
): (Boolean, Document.Node.Perspective_Text.T) = {
if (is_theory) {
- val snapshot = model.snapshot()
+ val snapshot = resources.snapshot(model)
val required = node_required || editor.document_node_required(node_name)
@@ -231,12 +232,6 @@
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
def is_stable: Boolean = pending_edits.isEmpty
- def snapshot(): Document.Snapshot =
- session.snapshot(node_name, pending_edits = pending_edits)
-
- def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
- new VSCode_Rendering(snapshot, model)
- def rendering(): VSCode_Rendering = rendering(snapshot())
/* syntax */