author | wenzelm |
Wed, 22 Jun 2022 14:26:11 +0200 | |
changeset 75592 | f72b88f2842c |
parent 75591 | abd110cb7327 |
child 75593 | 3e09396db078 |
--- a/src/Pure/General/bytes.ML Wed Jun 22 14:22:08 2022 +0200 +++ b/src/Pure/General/bytes.ML Wed Jun 22 14:26:11 2022 +0200 @@ -138,6 +138,9 @@ val buffer = build o fold add o Buffer.contents; + +(* IO *) + fun read_block limit = File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));