149 |
149 |
150 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*) |
150 (*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*) |
151 fun fold_lines f path a = open_input (fn file => |
151 fun fold_lines f path a = open_input (fn file => |
152 let |
152 let |
153 val split = split_last o String.fields (fn c => str c = "\n"); |
153 val split = split_last o String.fields (fn c => str c = "\n"); |
154 fun read buf x = |
154 fun read buf = |
155 (case split (TextIO.input file) of |
155 (case split (TextIO.input file) of |
156 ([], "") => (case Buffer.content buf of "" => x | line => f line x) |
156 ([], "") => (case Buffer.content buf of "" => I | line => f line) |
157 | ([], rest) => read (Buffer.add rest buf) x |
157 | ([], rest) => read (Buffer.add rest buf) |
158 | (line :: lines, rest) => |
158 | (line :: lines, rest) => |
159 read_rest (lines, rest) (f (Buffer.content (Buffer.add line buf)) x)) |
159 f (Buffer.content (Buffer.add line buf)) |
160 and read_rest (lines, rest) x = read (Buffer.add rest Buffer.empty) (fold f lines x); |
160 #> fold f lines |
|
161 #> read (Buffer.add rest Buffer.empty)); |
161 in read Buffer.empty a end) path; |
162 in read Buffer.empty a end) path; |
162 |
163 |
163 val read = open_input TextIO.inputAll; |
164 val read = open_input TextIO.inputAll; |
164 |
165 |
165 |
166 |