# HG changeset patch
# User wenzelm
# Date 1506452080 -7200
# Node ID 91500c024c7f46e37a952c2bd417613d6647734b
# Parent  41177b1240674769055704890584b8f705ed4658
tuned;

diff -r 41177b124067 -r 91500c024c7f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 26 17:32:16 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Sep 26 20:54:40 2017 +0200
@@ -64,6 +64,13 @@
     }
     else Nil
 
+  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
+  {
+    val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
+    val dir = Path.explode(name.master_dir)
+    loaded_files(syntax, text).map(a => dir + Path.explode(a))
+  }
+
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
diff -r 41177b124067 -r 91500c024c7f src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Sep 26 17:32:16 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Sep 26 20:54:40 2017 +0200
@@ -90,14 +90,8 @@
 
     def loaded_files: List[Path] =
     {
-      def loaded(dep: Thy_Info.Dep): List[Path] =
-      {
-        val string = resources.with_thy_reader(dep.name,
-          reader => Symbol.decode(reader.source.toString))
-        resources.loaded_files(syntax, string).
-          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
-      }
-      val dep_files = Par_List.map(loaded _, rev_deps)
+      val dep_files =
+        Par_List.map((dep: Thy_Info.Dep) => resources.loaded_files(syntax, dep.name), rev_deps)
       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
     }