# HG changeset patch
# User wenzelm
# Date 1670353731 -3600
# Node ID 6cd6c553b48094b3b47967323e173d193ac98d77
# Parent  127ee77c24ffdd776302ce5cc96d719defa25a06
clarified signature: less redundancy;

diff -r 127ee77c24ff -r 6cd6c553b480 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Dec 06 19:29:29 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Dec 06 20:08:51 2022 +0100
@@ -454,4 +454,26 @@
 
     override def toString: String = entries.toString
   }
+
+
+  /* resolve implicit theory dependencies */
+
+  def resolve_dependencies[A](
+    models: Map[A, Document.Model],
+    theories: List[(Document.Node.Name, Position.T)]
+  ): List[Document.Node.Name] = {
+    val model_theories =
+      (for (model <- models.valuesIterator 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
+        thy_name <- make_theory_name(model.node_name)
+      } yield thy_name).toList
+
+    thy_files1 ::: thy_files2
+  }
 }
diff -r 127ee77c24ff -r 6cd6c553b480 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 06 19:29:29 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 06 20:08:51 2022 +0100
@@ -208,26 +208,12 @@
     file_watcher: File_Watcher
   ): (Boolean, Boolean) = {
     state.change_result { st =>
-      /* theory files */
-
-      val thys =
-        (for ((_, model) <- st.models.iterator if model.is_theory)
-         yield (model.node_name, Position.none)).toList
-
-      val thy_files1 = resources.dependencies(thys).theories
-
-      val thy_files2 =
-        (for {
-          (_, model) <- st.models.iterator
-          thy_name <- resources.make_theory_name(model.node_name)
-        } yield thy_name).toList
-
-
-      /* auxiliary files */
+      val thy_files = resources.resolve_dependencies(st.models, Nil)
 
       val stable_tip_version =
-        if (st.models.forall(entry => entry._2.is_stable))
+        if (st.models.valuesIterator.forall(_.is_stable)) {
           session.get_state().stable_tip_version
+        }
         else None
 
       val aux_files =
@@ -236,12 +222,9 @@
           case None => Nil
         }
 
-
-      /* loaded models */
-
       val loaded_models =
         (for {
-          node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator
+          node_name <- thy_files.iterator ++ aux_files.iterator
           file = node_file(node_name)
           if !st.models.isDefinedAt(file)
           text <- { file_watcher.register_parent(file); read_file_content(node_name) }
diff -r 127ee77c24ff -r 6cd6c553b480 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 06 19:29:29 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 06 20:08:51 2022 +0100
@@ -114,21 +114,12 @@
     val required_files = {
       val models = Document_Model.get_models()
 
-      val thys =
-        (for ((node_name, model) <- models.iterator if model.is_theory)
-          yield (node_name, Position.none)).toList
-      val thy_files1 = resources.dependencies(thys).theories
-
-      val thy_files2 =
-        (for {
-          (node_name, _) <- models.iterator
-          thy_name <- resources.make_theory_name(node_name)
-        } yield thy_name).toList
+      val thy_files = resources.resolve_dependencies(models, Nil)
 
       val aux_files =
         if (options.bool("jedit_auto_resolve")) {
           val stable_tip_version =
-            if (models.forall(p => p._2.is_stable)) {
+            if (models.valuesIterator.forall(_.is_stable)) {
               session.get_state().stable_tip_version
             }
             else None
@@ -139,7 +130,7 @@
         }
         else Nil
 
-      (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
+      (thy_files ::: aux_files).filterNot(models.isDefinedAt)
     }
     if (required_files.nonEmpty) {
       try {