# HG changeset patch
# User wenzelm
# Date 1655901078 -7200
# Node ID 3e09396db0784deea61e0826491ec1558f8ee392
# Parent  f72b88f2842c5edc41bd6f479d83efeaa42310ac
tuned;

diff -r f72b88f2842c -r 3e09396db078 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jun 22 14:26:11 2022 +0200
+++ b/src/Pure/General/file.ML	Wed Jun 22 14:31:18 2022 +0200
@@ -147,13 +147,13 @@
   let
     fun read buf x =
       (case input file of
-        "" => (case Buffer.content buf of "" => x | line => f line x)
+        "" => (case Buffer.content buf of "" => x | chunk => f chunk x)
       | input =>
           (case String.fields (fn c => c = terminator) input of
             [rest] => read (Buffer.add rest buf) x
-          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
-    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
-      | read_lines (line :: more) x = read_lines more (f line x);
+          | chunk :: more => read_chunks more (f (Buffer.content (Buffer.add chunk buf)) x)))
+    and read_chunks [rest] x = read (Buffer.add rest Buffer.empty) x
+      | read_chunks (line :: more) x = read_chunks more (f line x);
   in read Buffer.empty a end) path;
 
 fun fold_lines f = fold_chunks #"\n" f;