src/Pure/General/file.ML
changeset 48911 5debc3e4fa81
parent 48446 8f611bc3650b
child 56533 cd8b6d849b6a
equal deleted inserted replaced
48910:1c8c15c30356 48911:5debc3e4fa81
   126 (* input *)
   126 (* input *)
   127 
   127 
   128 (*
   128 (*
   129   scalable iterator:
   129   scalable iterator:
   130   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   130   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   131   . optional terminator at end-of-file
   131   . optional terminator at end-of-input
   132 *)
   132 *)
   133 fun fold_chunks terminator f path a = open_input (fn file =>
   133 fun fold_chunks terminator f path a = open_input (fn file =>
   134   let
   134   let
   135     fun read buf x =
   135     fun read buf x =
   136       (case TextIO.input file of
   136       (case TextIO.input file of