# HG changeset patch
# User wenzelm
# Date 1607441417 -3600
# Node ID d0038b553e0e4ddad46dd733aa13af337b759f5b
# Parent  4cb480334f488d3043ce3cc92123b4ce7b0db6be
clarified signature: name according to db model without Sessions.Structure/Deps;

diff -r 4cb480334f48 -r d0038b553e0e src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Dec 07 22:28:41 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Tue Dec 08 16:30:17 2020 +0100
@@ -90,6 +90,12 @@
       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 4cb480334f48 -r d0038b553e0e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Mon Dec 07 22:28:41 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Tue Dec 08 16:30:17 2020 +0100
@@ -13,12 +13,10 @@
 object Build_Job
 {
   def read_theory(
-    db_context: Sessions.Database_Context, node_name: Document.Node.Name): Command =
+    db_context: Sessions.Database_Context, session: String, theory: String): Option[Command] =
   {
-    val session = db_context.sessions_structure.bootstrap.theory_qualifier(node_name)
-
     def read(name: String): Export.Entry =
-      db_context.get_export(session, node_name.theory, name)
+      db_context.get_export(session, theory, name)
 
     def read_xml(name: String): XML.Body =
       db_context.xml_cache.body(
@@ -26,17 +24,14 @@
 
     (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 blobs =
           blobs_files.map(file =>
           {
-            val master_dir =
-              Thy_Header.split_file_name(file) match {
-                case Some((dir, _)) => dir
-                case None => ""
-              }
+            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)
@@ -60,10 +55,11 @@
               index -> Markup_Tree.from_XML(xml)
             })
 
-        Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
-          blobs_info = blobs_info, results = results, markups = markups)
-
-      case _ => error("Malformed PIDE exports for theory " + node_name)
+        val command =
+          Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
+            blobs_info = blobs_info, results = results, markups = markups)
+        Some(command)
+      case _ => None
     }
   }
 }