author | wenzelm |
Fri, 12 Aug 2022 15:57:22 +0200 | |
changeset 75823 | 6eb8d6cdb686 |
parent 75822 | 0a14663dffcc |
child 75824 | a2b2e8964e1a |
--- 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)) }