# HG changeset patch
# User wenzelm
# Date 1720965418 -7200
# Node ID 36da6a3c79d6f91708da11bad10e6058a230dca8
# Parent  d55cdb87f3326c691436432b97f8f9af7c776f41
more scalable operations;

diff -r d55cdb87f332 -r 36da6a3c79d6 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sun Jul 14 15:50:42 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sun Jul 14 15:56:58 2024 +0200
@@ -24,6 +24,8 @@
   val body_size: XML.body -> int
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
+  val bytes_of_body: XML.body -> Bytes.T
+  val bytes_of: XML.tree -> Bytes.T
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
@@ -76,6 +78,9 @@
 val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
 val string_of = string_of_body o single;
 
+val bytes_of_body = Bytes.build o fold (traverse Bytes.add);
+val bytes_of = bytes_of_body o single;
+
 fun write_body path body =
   path |> File_Stream.open_output (fn file =>
     fold (traverse (fn s => fn () => File_Stream.output file s)) body ());