# HG changeset patch
# User wenzelm
# Date 1567086185 -7200
# Node ID b99b925dbd84d0c70e4899d8c0c715a2d4cda12c
# Parent  2bbd945728e25208700c73e9ffc19c57e4831d66
tuned signature;

diff -r 2bbd945728e2 -r b99b925dbd84 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Aug 29 14:20:46 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Aug 29 15:43:05 2019 +0200
@@ -132,6 +132,9 @@
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
+  def import_name(info: Sessions.Info, s: String): Document.Node.Name =
+    import_name(info.name, info.dir.implode, s)
+
   def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
   {
     val name = import_name(qualifier, dir, s)
@@ -246,12 +249,9 @@
   def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
     : Dependencies[Options] =
   {
-    val qualifier = info.name
-    val dir = info.dir.implode
-
     (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
       dependencies.require_thys(options,
-        for { (thy, pos) <- thys } yield (import_name(qualifier, dir, thy), pos),
+        for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
         progress = progress)
     })
   }