# HG changeset patch
# User wenzelm
# Date 1637150102 -3600
# Node ID 1f40ded31b78dae238f1138ddceefa64c17eeee6
# Parent  d540c36cd0d27b60c1e5facb45965ef2d73db627
clarified modules;

diff -r d540c36cd0d2 -r 1f40ded31b78 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Nov 17 12:28:07 2021 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 17 12:55:02 2021 +0100
@@ -292,4 +292,36 @@
     else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
     else path.file.setExecutable(flag, false)
   }
+
+
+  /* content */
+
+  object Content
+  {
+    def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content)
+    def apply(path: Path, content: String): Content = new Content_String(path, content)
+    def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
+  }
+
+  trait Content
+  {
+    def path: Path
+    def write(dir: Path): Unit
+  }
+
+  final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content
+  {
+    def write(dir: Path): Unit = Bytes.write(dir + path, content)
+  }
+
+  final class Content_String private[File](val path: Path, content: String) extends Content
+  {
+    def write(dir: Path): Unit = File.write(dir + path, content)
+  }
+
+  final class Content_XML private[File](val path: Path, content: XML.Body)
+  {
+    def output(out: XML.Body => String): Content_String =
+      new Content_String(path, out(content))
+  }
 }
diff -r d540c36cd0d2 -r 1f40ded31b78 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Nov 17 12:28:07 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Nov 17 12:55:02 2021 +0100
@@ -11,31 +11,6 @@
 {
   /* document variants */
 
-  object Content
-  {
-    def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content)
-    def apply(path: Path, content: String): Content = new Content_String(path, content)
-    def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
-  }
-  trait Content
-  {
-    def path: Path
-    def write(dir: Path): Unit
-  }
-  final class Content_Bytes private[Document_Build](val path: Path, content: Bytes) extends Content
-  {
-    def write(dir: Path): Unit = Bytes.write(dir + path, content)
-  }
-  final class Content_String private[Document_Build](val path: Path, content: String) extends Content
-  {
-    def write(dir: Path): Unit = File.write(dir + path, content)
-  }
-  final class Content_XML private[Document_Build](val path: Path, content: XML.Body)
-  {
-    def output(out: XML.Body => String): Content_String =
-      new Content_String(path, out(content))
-  }
-
   abstract class Document_Name
   {
     def name: String
@@ -62,7 +37,7 @@
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
-    def isabelletags: Content =
+    def isabelletags: File.Content =
     {
       val path = Path.explode("isabelletags.sty")
       val content =
@@ -74,7 +49,7 @@
               case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
               case cs => "\\isakeeptag{" + cs.mkString + "}"
             }))
-      Content(path, content)
+      File.Content(path, content)
     }
   }
 
@@ -218,31 +193,31 @@
     def session_theories: List[Document.Node.Name] = base.session_theories
     def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories
 
-    lazy val document_latex: List[Content_XML] =
+    lazy val document_latex: List[File.Content_XML] =
       for (name <- document_theories)
       yield {
         val path = Path.basic(tex_name(name))
         val content = YXML.parse_body(get_export(name.theory, Export.DOCUMENT_LATEX).text)
-        Content(path, content)
+        File.Content(path, content)
       }
 
-    lazy val session_graph: Content =
+    lazy val session_graph: File.Content =
     {
       val path = Presentation.session_graph_path
       val content = graphview.Graph_File.make_pdf(options, base.session_graph_display)
-      Content(path, content)
+      File.Content(path, content)
     }
 
-    lazy val session_tex: Content =
+    lazy val session_tex: File.Content =
     {
       val path = Path.basic("session.tex")
       val content =
         Library.terminate_lines(
           base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))
-      Content(path, content)
+      File.Content(path, content)
     }
 
-    lazy val isabelle_logo: Option[Content] =
+    lazy val isabelle_logo: Option[File.Content] =
     {
       document_logo.map(logo_name =>
         Isabelle_System.with_tmp_file("logo", ext = "pdf")(tmp_path =>
@@ -250,7 +225,7 @@
           Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
           val path = Path.basic("isabelle_logo.pdf")
           val content = Bytes.read(tmp_path)
-          Content(path, content)
+          File.Content(path, content)
         }))
     }