# HG changeset patch
# User wenzelm
# Date 1660313292 -7200
# Node ID ad00fbf64bff587e07b0528ff3cd76bf85b2e632
# Parent  a2b2e8964e1aa0164e7f4adc6808a4de0dd999b9
clarified signature --- simplified types;

diff -r a2b2e8964e1a -r ad00fbf64bff src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Aug 12 16:01:52 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Aug 12 16:08:12 2022 +0200
@@ -301,17 +301,13 @@
 
   /* content */
 
-  def content(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
-  def content(path: Path, content: String): Content_String = new Content_String(path, content)
+  def content(path: Path, content: Bytes): Content = new Content(path, content)
+  def content(path: Path, content: String): Content = new Content(path, Bytes(content))
   def content(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 private[File](val path: Path, val content: Bytes) {
     override def toString: String = path.toString
-  }
 
-  final class Content_Bytes private[File](val path: Path, val content: Bytes) extends Content {
     def write(dir: Path): Unit = {
       val full_path = dir + path
       Isabelle_System.make_directory(full_path.expand.dir)
@@ -319,18 +315,9 @@
     }
   }
 
-  final class Content_String private[File](val path: Path, val content: String) extends Content {
-    def write(dir: Path): Unit = {
-      val full_path = dir + path
-      Isabelle_System.make_directory(full_path.expand.dir)
-      File.write(full_path, content)
-    }
-  }
-
   final class Content_XML private[File](val path: Path, val content: XML.Body) {
     override def toString: String = path.toString
 
-    def output(out: XML.Body => String): Content_String =
-      new Content_String(path, out(content))
+    def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content)))
   }
 }
diff -r a2b2e8964e1a -r ad00fbf64bff src/Pure/System/classpath.scala
--- a/src/Pure/System/classpath.scala	Fri Aug 12 16:01:52 2022 +0200
+++ b/src/Pure/System/classpath.scala	Fri Aug 12 16:08:12 2022 +0200
@@ -20,7 +20,7 @@
 
   def apply(
     jar_files: List[JFile] = Nil,
-    jar_contents: List[File.Content_Bytes] = Nil): Classpath =
+    jar_contents: List[File.Content] = Nil): Classpath =
   {
     val jar_files0 =
       for {
diff -r a2b2e8964e1a -r ad00fbf64bff src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Aug 12 16:01:52 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Aug 12 16:08:12 2022 +0200
@@ -138,7 +138,7 @@
 
     override def toString: String = session
 
-    val classpath: List[File.Content_Bytes] = session_context.classpath()
+    val classpath: List[File.Content] = session_context.classpath()
 
     def document_bibliography: Boolean = options.bool("document_bibliography")
 
diff -r a2b2e8964e1a -r ad00fbf64bff src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 12 16:01:52 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 12 16:08:12 2022 +0200
@@ -411,7 +411,7 @@
     def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
       new Theory_Context(session_context, theory, other_cache)
 
-    def classpath(): List[File.Content_Bytes] = {
+    def classpath(): List[File.Content] = {
       (for {
         session <- session_stack.iterator
         info <- sessions_structure.get(session).iterator