# HG changeset patch
# User wenzelm
# Date 1315755001 -7200
# Node ID 3b6613366dd79b8f95d78c9c86476775491d0c7d
# Parent  1cbe20966cdb0823507886066b36096de5400869
more orthogonal signature;

diff -r 1cbe20966cdb -r 3b6613366dd7 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sun Sep 11 15:20:09 2011 +0200
+++ b/src/Pure/General/file.ML	Sun Sep 11 17:30:01 2011 +0200
@@ -27,6 +27,7 @@
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_lines: Path.T -> string list
+  val read_pages: Path.T -> string list
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -128,7 +129,11 @@
 
 (* input *)
 
-(*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
+(*
+  scalable iterator:
+  . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
+  . optional terminator at end-of-file
+*)
 fun fold_chunks terminator f path a = open_input (fn file =>
   let
     fun read buf x =
@@ -146,6 +151,7 @@
 fun fold_pages f = fold_chunks #"\f" f;
 
 fun read_lines path = rev (fold_lines cons path []);
+fun read_pages path = rev (fold_pages cons path []);
 
 val read = open_input TextIO.inputAll;