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

diff -r f848f66a8cb7 -r ad957ab06f72 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;