src/Tools/VSCode/src/vscode_model.scala
changeset 76765 c654103e9c9d
parent 76761 d062c7f4f2d1
child 76776 011759a7f2f6
--- 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 */