# HG changeset patch
# User wenzelm
# Date 1657545737 -7200
# Node ID 23fbdac78310000c6c193750381e9af646aaef91
# Parent  abd4db50ff1e1167e25e6fb7909f7b5d8c4d6a25
clarified signature;

diff -r abd4db50ff1e -r 23fbdac78310 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Jul 11 15:08:57 2022 +0200
+++ b/src/Pure/General/file.scala	Mon Jul 11 15:22:17 2022 +0200
@@ -296,8 +296,8 @@
   /* 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: Bytes): Content_Bytes = new Content_Bytes(path, content)
+    def apply(path: Path, content: String): Content_String = new Content_String(path, content)
     def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
   }
 
@@ -306,7 +306,7 @@
     def write(dir: Path): Unit
   }
 
-  final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content {
+  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)
@@ -314,7 +314,7 @@
     }
   }
 
-  final class Content_String private[File](val path: Path, content: String) extends Content {
+  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)
@@ -322,7 +322,7 @@
     }
   }
 
-  final class Content_XML private[File](val path: Path, content: XML.Body) {
+  final class Content_XML private[File](val path: Path, val content: XML.Body) {
     def output(out: XML.Body => String): Content_String =
       new Content_String(path, out(content))
   }