changeset 80425 | efa212a6699a |
parent 79819 | 141df3fb25bf |
child 80437 | 2c07b9b2f9f4 |
--- a/src/Pure/Tools/dump.scala Tue Jun 25 18:09:53 2024 +0200 +++ b/src/Pure/Tools/dump.scala Wed Jun 26 15:22:20 2024 +0200 @@ -33,8 +33,7 @@ write(file_name, Bytes(text)) def write(file_name: Path, body: XML.Body): Unit = - using(File.writer(write_path(file_name).file))( - writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body)) + write(file_name, Symbol.encode(YXML.string_of_body(body))) } sealed case class Aspect(