--- a/src/Pure/Thy/bibtex.scala Sun Jan 01 22:54:40 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala Mon Jan 02 11:57:57 2023 +0100
@@ -26,8 +26,7 @@
override def theory_suffix: String = "bibtex_file"
override def theory_content(name: String): String =
- """theory "bib" imports Pure begin bibtex_file """ +
- Outer_Syntax.quote_string(name) + """ end"""
+ """theory "bib" imports Pure begin bibtex_file "." end"""
override def theory_excluded(name: String): Boolean = name == "bib"
override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
--- a/src/Pure/Thy/file_format.scala Sun Jan 01 22:54:40 2023 +0100
+++ b/src/Pure/Thy/file_format.scala Mon Jan 02 11:57:57 2023 +0100
@@ -88,7 +88,8 @@
}
yield {
val node = resources.append_path(name.node, Path.explode(theory_suffix))
- Document.Node.Name(node, master_dir = name.master_dir, theory = theory)
+ val master_dir = Url.strip_base_name(node).getOrElse("")
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
}
--- a/src/Pure/Thy/sessions.scala Sun Jan 01 22:54:40 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Jan 02 11:57:57 2023 +0100
@@ -50,8 +50,7 @@
override def theory_suffix: String = "ROOTS_file"
override def theory_content(name: String): String =
- """theory "ROOTS" imports Pure begin ROOTS_file """ +
- Outer_Syntax.quote_string(name) + """ end"""
+ """theory "ROOTS" imports Pure begin ROOTS_file "." end"""
override def theory_excluded(name: String): Boolean = name == "ROOTS"
}