--- a/src/Pure/PIDE/byte_message.ML Sat Nov 02 12:11:00 2019 +0100
+++ b/src/Pure/PIDE/byte_message.ML Sat Nov 02 12:32:38 2019 +0100
@@ -23,7 +23,7 @@
(* output operations *)
-fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s));
+fun write stream = List.app (File.output stream);
fun flush stream = ignore (try BinIO.flushOut stream);
--- a/src/Pure/PIDE/yxml.ML Sat Nov 02 12:11:00 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML Sat Nov 02 12:32:38 2019 +0100
@@ -84,7 +84,7 @@
fun write_body path body =
path |> File.open_output (fn file =>
- fold (traverse (fn s => fn () => BinIO.output (file, Byte.stringToBytes s))) body ());
+ fold (traverse (fn s => fn () => File.output file s)) body ());
(* markup elements *)