# HG changeset patch
# User huffman
# Date 1315762250 25200
# Node ID 19692967eb4664b51932f3cf6b55ce22c5a17441
# Parent  02efd5a6b6e5d3f71913dd4313de4b776acc3ea4# Parent  3b6613366dd79b8f95d78c9c86476775491d0c7d
merged

diff -r 02efd5a6b6e5 -r 19692967eb46 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sun Sep 11 09:40:18 2011 -0700
+++ b/src/Pure/General/file.ML	Sun Sep 11 10:30:50 2011 -0700
@@ -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;