# HG changeset patch
# User wenzelm
# Date 1655818818 -7200
# Node ID 4fc8a35579b2bac505fe8d3dd2cb2aee89ec2bc8
# Parent  833f26c3a3aff74e5e01380a13617da1637837dd
tuned signature;

diff -r 833f26c3a3af -r 4fc8a35579b2 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;