tuned;
authorwenzelm
Sat, 02 Nov 2019 12:32:38 +0100
changeset 70993 2e610951f79a
parent 70992 e7dfc505de1b
child 70994 ff11af12dfdd
tuned;
src/Pure/PIDE/byte_message.ML
src/Pure/PIDE/yxml.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);
 
--- 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 *)