proper execution of Bytes.write;
authorwenzelm
Thu, 23 Jun 2022 21:25:23 +0200
changeset 75602 7a0d4c126f79
parent 75597 e6e0a95f87f3
child 75603 fc8d64a578e4
proper execution of Bytes.write; tuned;
src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Wed Jun 22 17:07:00 2022 +0200
+++ b/src/Pure/General/bytes.ML	Thu Jun 23 21:25:23 2022 +0200
@@ -196,10 +196,12 @@
       | s => read (add s bytes))
   in read empty end;
 
-fun write_stream stream = File.outputs stream o contents;
+fun write_stream stream bytes =
+  File.outputs stream (contents bytes);
 
-val read = File.open_input (read_stream ~1);
-val write = File.open_output write_stream;
+fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+
+fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
 
 
 (* ML pretty printing *)