# HG changeset patch
# User wenzelm
# Date 1671832109 -3600
# Node ID 235de80d4b25e75d4d57ef71be262f5342da6a94
# Parent  c654103e9c9d2c7b2106a9843f516f1d8a008737
tuned signature;

diff -r c654103e9c9d -r 235de80d4b25 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 23 22:48:29 2022 +0100
@@ -458,18 +458,18 @@
   /* resolve implicit theory dependencies */
 
   def resolve_dependencies[A](
-    models: Map[A, Document.Model],
+    models: Iterable[Document.Model],
     theories: List[(Document.Node.Name, Position.T)]
   ): List[Document.Node.Name] = {
     val model_theories =
-      (for (model <- models.valuesIterator if model.is_theory)
+      (for (model <- models.iterator if model.is_theory)
         yield (model.node_name, Position.none)).toList
 
     val thy_files1 = dependencies(model_theories ::: theories).theories
 
     val thy_files2 =
       (for {
-        model <- models.valuesIterator if !model.is_theory
+        model <- models.iterator if !model.is_theory
         thy_name <- make_theory_name(model.node_name)
       } yield thy_name).toList
 
diff -r c654103e9c9d -r 235de80d4b25 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Dec 23 22:48:29 2022 +0100
@@ -697,8 +697,8 @@
     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.forall(p => p._2.pending_edits.isEmpty)) get_state().stable_tip_version
+  def stable_tip_version[A](models: Iterable[Document.Model]): Option[Document.Version] =
+    if (models.forall(model => model.pending_edits.isEmpty)) get_state().stable_tip_version
     else None
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot = {
diff -r c654103e9c9d -r 235de80d4b25 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:48:29 2022 +0100
@@ -235,10 +235,10 @@
     file_watcher: File_Watcher
   ): (Boolean, Boolean) = {
     state.change_result { st =>
-      val stable_tip_version = session.stable_tip_version(st.models)
+      val stable_tip_version = session.stable_tip_version(st.models.values)
 
       val thy_files =
-        resources.resolve_dependencies(st.models,
+        resources.resolve_dependencies(st.models.values,
           editor.document_required().map((_, Position.none)))
 
       val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
diff -r c654103e9c9d -r 235de80d4b25 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:41:47 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:48:29 2022 +0100
@@ -113,12 +113,12 @@
       val models = Document_Model.get_models()
 
       val thy_files =
-        resources.resolve_dependencies(models,
+        resources.resolve_dependencies(models.values,
           PIDE.editor.document_required().map((_, Position.none)))
 
       val aux_files =
         if (resources.auto_resolve) {
-          session.stable_tip_version(models) match {
+          session.stable_tip_version(models.values) match {
             case Some(version) => resources.undefined_blobs(version)
             case None => delay_load.invoke(); Nil
           }