# HG changeset patch
# User wenzelm
# Date 1310829109 -7200
# Node ID d89353d17f54ff353cca29188940e4110c3efcd1
# Parent  33e20b7d7e7286db50c02aee85ad16313f314ea6
added File.fold_pages for streaming of large files;
prefer \f notation;

diff -r 33e20b7d7e72 -r d89353d17f54 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Jul 16 16:51:12 2011 +0200
+++ b/src/Pure/General/file.ML	Sat Jul 16 17:11:49 2011 +0200
@@ -22,6 +22,7 @@
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
+  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -110,19 +111,22 @@
 (* input *)
 
 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
-fun fold_lines f path a = open_input (fn file =>
+fun fold_chunks terminator 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 (fn c => c = #"\n") input of
+          (case String.fields (fn c => c = terminator) input of
             [rest] => read (Buffer.add rest buf) 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 = fold_chunks #"\n" f;
+fun fold_pages f = fold_chunks #"\f" f;
+
 val read = open_input TextIO.inputAll;
 
 
diff -r 33e20b7d7e72 -r d89353d17f54 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Jul 16 16:51:12 2011 +0200
+++ b/src/Pure/General/symbol.ML	Sat Jul 16 17:11:49 2011 +0200
@@ -151,7 +151,7 @@
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
-  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
+  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\f" => true | "\^M" => true
     | _ => false;
 
 fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
diff -r 33e20b7d7e72 -r d89353d17f54 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Jul 16 16:51:12 2011 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Jul 16 17:11:49 2011 +0200
@@ -64,6 +64,7 @@
   else if s = "\\" then "\\\\"
   else if s = "\t" then "\\t"
   else if s = "\n" then "\\n"
+  else if s = "\f" then "\\f"
   else if s = "\r" then "\\r"
   else
     let val c = ord s in