# HG changeset patch
# User wenzelm
# Date 1719439777 -7200
# Node ID c92356464bb347a30c4a1c1097aae538cbf24275
# Parent  7d2922f0ae2be910cc7a0101066b8d59b3435fe1
more operations;

diff -r 7d2922f0ae2b -r c92356464bb3 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Thu Jun 27 00:01:01 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Thu Jun 27 00:09:37 2024 +0200
@@ -69,12 +69,23 @@
     def result(t: XML.Tree): String = { tree(t); builder.toString }
   }
 
+  class Output_Bytes(builder: Bytes.Builder) extends Output {
+    override def byte(b: Byte): Unit = { builder += b }
+    override def string(s: String): Unit = { builder += s }
+  }
+
   def string_of_body(body: XML.Body): String =
     new Output_String(new StringBuilder).result(body)
 
   def string_of_tree(tree: XML.Tree): String =
     new Output_String(new StringBuilder).result(tree)
 
+  def bytes_of_body(body: XML.Body): Bytes =
+    Bytes.Builder.use()(builder => new Output_Bytes(builder).trees(body))
+
+  def bytes_of_tree(tree: XML.Tree): Bytes =
+    Bytes.Builder.use()(builder => new Output_Bytes(builder).tree(tree))
+
 
   /* parsing */