src/Pure/General/file.ML
changeset 43845 d89353d17f54
parent 43616 9e237a9dc1fd
child 43848 8f2bf02a0ccb
     1.1 --- a/src/Pure/General/file.ML	Sat Jul 16 16:51:12 2011 +0200
     1.2 +++ b/src/Pure/General/file.ML	Sat Jul 16 17:11:49 2011 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
     1.5    val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
     1.6    val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
     1.7 +  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
     1.8    val read: Path.T -> string
     1.9    val write: Path.T -> string -> unit
    1.10    val append: Path.T -> string -> unit
    1.11 @@ -110,19 +111,22 @@
    1.12  (* input *)
    1.13  
    1.14  (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
    1.15 -fun fold_lines f path a = open_input (fn file =>
    1.16 +fun fold_chunks terminator f path a = open_input (fn file =>
    1.17    let
    1.18      fun read buf x =
    1.19        (case TextIO.input file of
    1.20          "" => (case Buffer.content buf of "" => x | line => f line x)
    1.21        | input =>
    1.22 -          (case String.fields (fn c => c = #"\n") input of
    1.23 +          (case String.fields (fn c => c = terminator) input of
    1.24              [rest] => read (Buffer.add rest buf) x
    1.25            | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
    1.26      and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
    1.27        | read_lines (line :: more) x = read_lines more (f line x);
    1.28    in read Buffer.empty a end) path;
    1.29  
    1.30 +fun fold_lines f = fold_chunks #"\n" f;
    1.31 +fun fold_pages f = fold_chunks #"\f" f;
    1.32 +
    1.33  val read = open_input TextIO.inputAll;
    1.34  
    1.35