--- a/src/Pure/General/file.scala Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/General/file.scala Fri Aug 12 16:01:52 2022 +0200
@@ -301,11 +301,9 @@
/* content */
- object 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)
- }
+ 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: XML.Body): Content_XML = new Content_XML(path, content)
trait Content {
def path: Path