--- a/src/Pure/General/bytes.ML Tue Jun 21 14:46:42 2022 +0200
+++ b/src/Pure/General/bytes.ML Tue Jun 21 14:51:17 2022 +0200
@@ -81,8 +81,7 @@
| s => read_bytes (add s bytes))
in read_bytes empty end;
-fun write_stream stream bytes =
- List.app (File.output stream) (contents bytes);
+fun write_stream stream = File.outputs stream o contents;
val read = File.open_input read_stream;
val write = File.open_output write_stream;
--- a/src/Pure/General/file.ML Tue Jun 21 14:46:42 2022 +0200
+++ b/src/Pure/General/file.ML Tue Jun 21 14:51:17 2022 +0200
@@ -38,6 +38,7 @@
val append: Path.T -> string -> unit
val generate: Path.T -> string -> unit
val output: BinIO.outstream -> string -> unit
+ val outputs: BinIO.outstream -> string list -> unit
val write_list: Path.T -> string list -> unit
val append_list: Path.T -> string list -> unit
val write_buffer: Path.T -> Buffer.T -> unit
@@ -167,6 +168,7 @@
(* output *)
fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
+val outputs = List.app o output;
fun output_list txts file = List.app (output file) txts;
fun write_list path txts = open_output (output_list txts) path;
--- a/src/Pure/PIDE/byte_message.ML Tue Jun 21 14:46:42 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML Tue Jun 21 14:51:17 2022 +0200
@@ -25,7 +25,7 @@
(* output operations *)
-fun write stream = List.app (File.output stream);
+val write = File.outputs;
fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree ();