tuned signature: more operations;
authorwenzelm
Tue, 21 Jun 2022 14:51:17 +0200
changeset 75571 ac5e633ad9b3
parent 75570 ad957ab06f72
child 75572 833f26c3a3af
tuned signature: more operations;
src/Pure/General/bytes.ML
src/Pure/General/file.ML
src/Pure/PIDE/byte_message.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;
--- 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 ();