tuned signature;
authorwenzelm
Tue, 21 Jun 2022 15:40:18 +0200
changeset 75573 4fc8a35579b2
parent 75572 833f26c3a3af
child 75574 5945c6f5126a
tuned signature;
src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Tue Jun 21 14:51:50 2022 +0200
+++ b/src/Pure/General/bytes.ML	Tue Jun 21 15:40:18 2022 +0200
@@ -22,6 +22,7 @@
   val build: (T -> T) -> T
   val string: string -> T
   val buffer: Buffer.T -> T
+  val read_chunk: BinIO.instream -> string
   val read_stream: BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
   val read: Path.T -> T
@@ -75,10 +76,12 @@
 
 val buffer = build o fold add o Buffer.contents;
 
+val read_chunk = File.input_size chunk_size;
+
 fun read_stream stream =
   let
     fun read_bytes bytes =
-      (case File.input_size chunk_size stream of
+      (case read_chunk stream of
         "" => bytes
       | s => read_bytes (add s bytes))
   in read_bytes empty end;