tuned comments;
authorwenzelm
Wed, 22 Jun 2022 14:26:11 +0200
changeset 75592 f72b88f2842c
parent 75591 abd110cb7327
child 75593 3e09396db078
tuned comments;
src/Pure/General/bytes.ML
--- 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));