src/Pure/General/file.ML
changeset 44879 3b6613366dd7
parent 43848 8f2bf02a0ccb
child 48446 8f611bc3650b
equal deleted inserted replaced
44878:1cbe20966cdb 44879:3b6613366dd7
    25   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    25   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    26   val read_dir: Path.T -> string list
    26   val read_dir: Path.T -> string list
    27   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    27   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    28   val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    28   val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
    29   val read_lines: Path.T -> string list
    29   val read_lines: Path.T -> string list
       
    30   val read_pages: Path.T -> string list
    30   val read: Path.T -> string
    31   val read: Path.T -> string
    31   val write: Path.T -> string -> unit
    32   val write: Path.T -> string -> unit
    32   val append: Path.T -> string -> unit
    33   val append: Path.T -> string -> unit
    33   val write_list: Path.T -> string list -> unit
    34   val write_list: Path.T -> string list -> unit
    34   val append_list: Path.T -> string list -> unit
    35   val append_list: Path.T -> string list -> unit
   126 fun read_dir path = rev (fold_dir cons path []);
   127 fun read_dir path = rev (fold_dir cons path []);
   127 
   128 
   128 
   129 
   129 (* input *)
   130 (* input *)
   130 
   131 
   131 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
   132 (*
       
   133   scalable iterator:
       
   134   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
       
   135   . optional terminator at end-of-file
       
   136 *)
   132 fun fold_chunks terminator f path a = open_input (fn file =>
   137 fun fold_chunks terminator f path a = open_input (fn file =>
   133   let
   138   let
   134     fun read buf x =
   139     fun read buf x =
   135       (case TextIO.input file of
   140       (case TextIO.input file of
   136         "" => (case Buffer.content buf of "" => x | line => f line x)
   141         "" => (case Buffer.content buf of "" => x | line => f line x)
   144 
   149 
   145 fun fold_lines f = fold_chunks #"\n" f;
   150 fun fold_lines f = fold_chunks #"\n" f;
   146 fun fold_pages f = fold_chunks #"\f" f;
   151 fun fold_pages f = fold_chunks #"\f" f;
   147 
   152 
   148 fun read_lines path = rev (fold_lines cons path []);
   153 fun read_lines path = rev (fold_lines cons path []);
       
   154 fun read_pages path = rev (fold_pages cons path []);
   149 
   155 
   150 val read = open_input TextIO.inputAll;
   156 val read = open_input TextIO.inputAll;
   151 
   157 
   152 
   158 
   153 (* output *)
   159 (* output *)