# HG changeset patch
# User wenzelm
# Date 1219948180 -7200
# Node ID 56e3a695434f78dec97b5f84be0106900801e74e
# Parent  7cef47b53febe4fb3f6ebb9b63b4bf702536c0e1
tuned fold_lines;

diff -r 7cef47b53feb -r 56e3a695434f src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Aug 28 20:19:45 2008 +0200
+++ b/src/Pure/General/file.ML	Thu Aug 28 20:29:40 2008 +0200
@@ -151,13 +151,14 @@
 fun fold_lines f path a = open_input (fn file =>
   let
     val split = split_last o String.fields (fn c => str c = "\n");
-    fun read buf x =
+    fun read buf =
       (case split (TextIO.input file) of
-        ([], "") => (case Buffer.content buf of "" => x | line => f line x)
-      | ([], rest) => read (Buffer.add rest buf) x
+        ([], "") => (case Buffer.content buf of "" => I | line => f line)
+      | ([], rest) => read (Buffer.add rest buf)
       | (line :: lines, rest) =>
-          read_rest (lines, rest) (f (Buffer.content (Buffer.add line buf)) x))
-    and read_rest (lines, rest) x = read (Buffer.add rest Buffer.empty) (fold f lines x);
+          f (Buffer.content (Buffer.add line buf))
+          #> fold f lines
+          #> read (Buffer.add rest Buffer.empty));
   in read Buffer.empty a end) path;
 
 val read = open_input TextIO.inputAll;