# HG changeset patch
# User wenzelm
# Date 1572694358 -3600
# Node ID 2e610951f79a152381875c3837c21bf778d3f1c7
# Parent  e7dfc505de1bfbc01f412548b70695ab74f36fc6
tuned;

diff -r e7dfc505de1b -r 2e610951f79a src/Pure/PIDE/byte_message.ML
--- 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);
 
diff -r e7dfc505de1b -r 2e610951f79a src/Pure/PIDE/yxml.ML
--- 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 *)