--- 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 ());