# HG changeset patch
# User noschinl
# Date 1309521265 -7200
# Node ID 9e237a9dc1fddf7a7088d08a31bda6db235bc974
# Parent  8e0f6cfa8eb252e302f761ba795e252a230fd7d8
reverted 782991e4180d: fold_fields was never used

diff -r 8e0f6cfa8eb2 -r 9e237a9dc1fd src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri Jul 01 13:54:23 2011 +0200
+++ b/src/Pure/General/file.ML	Fri Jul 01 13:54:25 2011 +0200
@@ -21,7 +21,6 @@
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
-  val fold_fields: (char -> bool) -> (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read: Path.T -> string
   val write: Path.T -> string -> unit
@@ -111,21 +110,19 @@
 (* input *)
 
 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
-fun fold_fields sep f path a = open_input (fn file =>
+fun fold_lines f path a = open_input (fn file =>
   let
     fun read buf x =
       (case TextIO.input file of
         "" => (case Buffer.content buf of "" => x | line => f line x)
       | input =>
-          (case String.fields sep input of
+          (case String.fields (fn c => c = #"\n") input of
             [rest] => read (Buffer.add rest buf) x
-          | field :: more => read_fields more (f (Buffer.content (Buffer.add field buf)) x)))
-    and read_fields [rest] x = read (Buffer.add rest Buffer.empty) x
-      | read_fields (field :: more) x = read_fields more (f field 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);
   in read Buffer.empty a end) path;
 
-fun fold_lines f path a = fold_fields (fn c => c = #"\n") f path a;
-
 val read = open_input TextIO.inputAll;