--- a/src/Pure/Tools/build_job.scala Fri Aug 19 21:04:14 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Fri Aug 19 21:25:13 2022 +0200
@@ -29,7 +29,13 @@
(thy_file, blobs_files) <- theory_context.files(permissive = true)
}
yield {
- val node_name = Resources.file_node(Path.explode(thy_file), theory = theory_context.theory)
+ val master_dir =
+ Thy_Header.split_file_name(thy_file) match {
+ case Some((dir, _)) => dir
+ case None => error("Cannot determine theory master directory: " + quote(thy_file))
+ }
+ val node_name =
+ Document.Node.Name(thy_file, master_dir = master_dir, theory = theory_context.theory)
val results =
Command.Results.make(
@@ -38,8 +44,8 @@
val blobs =
blobs_files.map { file =>
+ val name = Document.Node.Name(file)
val path = Path.explode(file)
- val name = Resources.file_node(path)
val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
Command.Blob(name, src_path, None)
}