--- a/src/Pure/PIDE/yxml.ML Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML Sat Nov 02 12:02:27 2019 +0100
@@ -25,6 +25,7 @@
val chunks_of_body: XML.body -> string list
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
+ val write_body: Path.T -> XML.body -> unit
val output_markup: Markup.T -> string * string
val output_markup_elem: Markup.T -> (string * string) * string
val parse_body: string -> XML.body
@@ -81,6 +82,10 @@
fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content;
val string_of = string_of_body o single;
+fun write_body path body =
+ path |> File.open_output (fn file =>
+ fold (traverse (fn s => fn () => BinIO.output (file, Byte.stringToBytes s))) body ());
+
(* markup elements *)