# HG changeset patch
# User wenzelm
# Date 1672657077 -3600
# Node ID 6e1bf28d5a80c21e7dc8ad3a3e9c24127497f721
# Parent  39db5e268aaff0751dc0cd951f02adc3291460c9
more standard master_dir;

diff -r 39db5e268aaf -r 6e1bf28d5a80 src/Pure/Thy/bibtex.scala
--- 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] = {
diff -r 39db5e268aaf -r 6e1bf28d5a80 src/Pure/Thy/file_format.scala
--- 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)
     }
   }
 
diff -r 39db5e268aaf -r 6e1bf28d5a80 src/Pure/Thy/sessions.scala
--- 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"
   }