# 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 */