src/Pure/PIDE/session.scala
changeset 76765 c654103e9c9d
parent 76761 d062c7f4f2d1
child 76766 235de80d4b25
--- a/src/Pure/PIDE/session.scala	Fri Dec 23 22:33:14 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Dec 23 22:41:47 2022 +0100
@@ -688,16 +688,17 @@
     else Document.State.init
   }
 
-  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
-      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
-    get_state().snapshot(name, pending_edits = pending_edits)
+  def snapshot(
+    node_name: Document.Node.Name = Document.Node.Name.empty,
+    pending_edits: Document.Pending_Edits = Document.Pending_Edits.empty
+  ): Document.Snapshot = get_state().snapshot(node_name = node_name, pending_edits = pending_edits)
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.session_base.overall_syntax
 
   def stable_tip_version[A](models: Map[A, Document.Model]): Option[Document.Version] =
-    if (models.valuesIterator.forall(_.is_stable)) get_state().stable_tip_version
+    if (models.forall(p => p._2.pending_edits.isEmpty)) get_state().stable_tip_version
     else None
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot = {