more standard master_dir;
authorwenzelm
Mon, 02 Jan 2023 11:57:57 +0100
changeset 76859 6e1bf28d5a80
parent 76858 39db5e268aaf
child 76860 f95ed5a0600c
more standard master_dir;
src/Pure/Thy/bibtex.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/sessions.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] = {
--- 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"
   }