# HG changeset patch
# User wenzelm
# Date 1607525625 -3600
# Node ID a9e091ccd450d0cb3595919a94d31adb6d0a7c72
# Parent  3a27e6f83ce160d625c1a26aea8761dcb6373956
clarified signature;

diff -r 3a27e6f83ce1 -r a9e091ccd450 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Dec 09 15:14:24 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Dec 09 15:53:45 2020 +0100
@@ -69,7 +69,7 @@
   def append(node_name: Document.Node.Name, source_path: Path): String =
     append(node_name.master_dir, source_path)
 
-  def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name =
+  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
   {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)
@@ -155,13 +155,13 @@
         case None => Nil
       }
     dirs.collectFirst({
-      case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) })
+      case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) })
   }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
-    def theory_node = make_theory_node(dir, Path.explode(s).thy, theory)
+    def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
diff -r 3a27e6f83ce1 -r a9e091ccd450 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Dec 09 15:14:24 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Dec 09 15:53:45 2020 +0100
@@ -90,12 +90,6 @@
       case _ => None
     }
 
-  def dir_name(s: String): String =
-    split_file_name(s) match {
-      case Some((dir, _)) => dir
-      case None => ""
-    }
-
   def import_name(s: String): String =
     s match {
       case File_Name(name) if !name.endsWith(".thy") => name
diff -r 3a27e6f83ce1 -r a9e091ccd450 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Dec 09 15:14:24 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Dec 09 15:53:45 2020 +0100
@@ -15,7 +15,10 @@
   /* theory markup/messages from database */
 
   def read_theory(
-    db_context: Sessions.Database_Context, session: String, theory: String): Option[Command] =
+    db_context: Sessions.Database_Context,
+    resources: Resources,
+    session: String,
+    theory: String): Option[Command] =
   {
     def read(name: String): Export.Entry =
       db_context.get_export(List(session), theory, name)
@@ -26,17 +29,16 @@
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
-        val node_name = Document.Node.Name(thy_file, Thy_Header.dir_name(thy_file), theory)
         val thy_path = Path.explode(thy_file)
         val thy_source = Symbol.decode(File.read(thy_path))
+        val node_name = resources.file_node(thy_path, theory = theory)
 
         val blobs =
           blobs_files.map(file =>
           {
-            val master_dir = Thy_Header.dir_name(file)
             val path = Path.explode(file)
             val src_path = File.relative_path(thy_path, path).getOrElse(path)
-            Command.Blob.read_file(Document.Node.Name(file, master_dir), src_path)
+            Command.Blob.read_file(resources.file_node(path), src_path)
           })
         val blobs_info = Command.Blobs_Info(blobs.map(Exn.Res(_)))