more scalable operations;
authorwenzelm
Sun, 14 Jul 2024 15:56:58 +0200
changeset 80563 36da6a3c79d6
parent 80562 d55cdb87f332
child 80564 2309ac831dd4
more scalable operations;
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 ());