# HG changeset patch
# User wenzelm
# Date 1655815877 -7200
# Node ID ac5e633ad9b380503e638acad1fc64ca0d0a17c4
# Parent  ad957ab06f72fcfbbc606a18701e1c18c33db876
tuned signature: more operations;

diff -r ad957ab06f72 -r ac5e633ad9b3 src/Pure/General/bytes.ML
--- 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;
diff -r ad957ab06f72 -r ac5e633ad9b3 src/Pure/General/file.ML
--- 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;
diff -r ad957ab06f72 -r ac5e633ad9b3 src/Pure/PIDE/byte_message.ML
--- 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 ();