--- a/src/Pure/Tools/build_job.scala Fri Dec 30 16:23:32 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Dec 30 20:26:28 2022 +0100
@@ -31,10 +31,8 @@
}
yield {
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))
- }
+ Url.strip_base_name(thy_file).getOrElse(
+ 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)