diff -r 0a14663dffcc -r 6eb8d6cdb686 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Fri Aug 12 15:48:47 2022 +0200 +++ b/src/Pure/General/file.scala Fri Aug 12 15:57:22 2022 +0200 @@ -330,6 +330,8 @@ } 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)) }