tuned signature: more operations;
authorwenzelm
Tue, 21 Jun 2022 14:46:42 +0200
changeset 75570 ad957ab06f72
parent 75569 f848f66a8cb7
child 75571 ac5e633ad9b3
tuned signature: more operations;
src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Tue Jun 21 14:22:34 2022 +0200
+++ b/src/Pure/General/bytes.ML	Tue Jun 21 14:46:42 2022 +0200
@@ -20,7 +20,10 @@
   val build: (T -> T) -> T
   val string: string -> T
   val buffer: Buffer.T -> T
+  val read_stream: BinIO.instream -> T
+  val write_stream: BinIO.outstream -> T -> unit
   val read: Path.T -> T
+  val write: Path.T -> T -> unit
 end;
 
 structure Bytes: BYTES =
@@ -70,12 +73,18 @@
 
 val buffer = build o fold add o Buffer.contents;
 
-val read = File.open_input (fn stream =>
+fun read_stream stream =
   let
     fun read_bytes bytes =
       (case File.input_size chunk_size stream of
         "" => bytes
       | s => read_bytes (add s bytes))
-  in read_bytes empty end);
+  in read_bytes empty end;
+
+fun write_stream stream bytes =
+  List.app (File.output stream) (contents bytes);
+
+val read = File.open_input read_stream;
+val write = File.open_output write_stream;
 
 end;