# HG changeset patch
# User wenzelm
# Date 1671832307 -3600
# Node ID 540cd80c5af2c07f2a6066d02777d0646056d536
# Parent  235de80d4b25e75d4d57ef71be262f5342da6a94
tuned signature;

diff -r 235de80d4b25 -r 540cd80c5af2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Dec 23 22:48:29 2022 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Dec 23 22:51:47 2022 +0100
@@ -459,13 +459,14 @@
 
   def resolve_dependencies[A](
     models: Iterable[Document.Model],
-    theories: List[(Document.Node.Name, Position.T)]
+    theories: List[Document.Node.Name]
   ): List[Document.Node.Name] = {
     val model_theories =
       (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_files1 =
+      dependencies(model_theories ::: theories.map((_, Position.none))).theories
 
     val thy_files2 =
       (for {
diff -r 235de80d4b25 -r 540cd80c5af2 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:48:29 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 23 22:51:47 2022 +0100
@@ -238,8 +238,7 @@
       val stable_tip_version = session.stable_tip_version(st.models.values)
 
       val thy_files =
-        resources.resolve_dependencies(st.models.values,
-          editor.document_required().map((_, Position.none)))
+        resources.resolve_dependencies(st.models.values, editor.document_required())
 
       val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
 
diff -r 235de80d4b25 -r 540cd80c5af2 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:48:29 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Dec 23 22:51:47 2022 +0100
@@ -113,8 +113,7 @@
       val models = Document_Model.get_models()
 
       val thy_files =
-        resources.resolve_dependencies(models.values,
-          PIDE.editor.document_required().map((_, Position.none)))
+        resources.resolve_dependencies(models.values, PIDE.editor.document_required())
 
       val aux_files =
         if (resources.auto_resolve) {