src/Pure/Tools/dump.scala
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(