added File.fold_pages for streaming of large files;
authorwenzelm
Sat Jul 16 17:11:49 2011 +0200 (2011-07-16)
changeset 43845d89353d17f54
parent 43844 33e20b7d7e72
child 43846 e6226e100ac5
added File.fold_pages for streaming of large files;
prefer \f notation;
src/Pure/General/file.ML
src/Pure/General/symbol.ML
src/Pure/ML/ml_syntax.ML
     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  
     2.1 --- a/src/Pure/General/symbol.ML	Sat Jul 16 16:51:12 2011 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Sat Jul 16 17:11:49 2011 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4    | is_ascii_quasi _ = false;
     2.5  
     2.6  val is_ascii_blank =
     2.7 -  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
     2.8 +  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     2.9      | _ => false;
    2.10  
    2.11  fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
     3.1 --- a/src/Pure/ML/ml_syntax.ML	Sat Jul 16 16:51:12 2011 +0200
     3.2 +++ b/src/Pure/ML/ml_syntax.ML	Sat Jul 16 17:11:49 2011 +0200
     3.3 @@ -64,6 +64,7 @@
     3.4    else if s = "\\" then "\\\\"
     3.5    else if s = "\t" then "\\t"
     3.6    else if s = "\n" then "\\n"
     3.7 +  else if s = "\f" then "\\f"
     3.8    else if s = "\r" then "\\r"
     3.9    else
    3.10      let val c = ord s in