src/Pure/General/file.ML
changeset 28510 66b95e857bde
parent 28500 4b79e5d3d0aa
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/General/file.ML	Mon Oct 06 22:35:03 2008 +0200
     1.2 +++ b/src/Pure/General/file.ML	Mon Oct 06 22:41:21 2008 +0200
     1.3 @@ -150,15 +150,15 @@
     1.4  (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
     1.5  fun fold_lines f path a = open_input (fn file =>
     1.6    let
     1.7 -    val split = split_last o String.fields (fn c => str c = "\n");
     1.8 -    fun read buf =
     1.9 -      (case split (TextIO.input file) of
    1.10 -        ([], "") => (case Buffer.content buf of "" => I | line => f line)
    1.11 -      | ([], rest) => read (Buffer.add rest buf)
    1.12 -      | (line :: lines, rest) =>
    1.13 -          f (Buffer.content (Buffer.add line buf))
    1.14 -          #> fold f lines
    1.15 -          #> read (Buffer.add rest Buffer.empty));
    1.16 +    fun read buf x =
    1.17 +      (case TextIO.input file of
    1.18 +        "" => (case Buffer.content buf of "" => x | line => f line x)
    1.19 +      | input =>
    1.20 +          (case String.fields (fn c => c = #"\n") input of
    1.21 +            [rest] => read (Buffer.add rest buf) x
    1.22 +          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
    1.23 +    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
    1.24 +      | read_lines (line :: more) x = read_lines more (f line x);
    1.25    in read Buffer.empty a end) path;
    1.26  
    1.27  val read = open_input TextIO.inputAll;