diff -r 10f155d5f34b -r c654103e9c9d src/Pure/PIDE/session.scala --- 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 = {