equal
deleted
inserted
replaced
148 (* input *) |
148 (* input *) |
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 fun read buf x = |
154 fun read buf = |
154 (case TextIO.input file of |
155 (case split (TextIO.input file) of |
155 "" => (case Buffer.content buf of "" => x | line => f line x) |
156 ([], "") => (case Buffer.content buf of "" => I | line => f line) |
156 | input => |
157 | ([], rest) => read (Buffer.add rest buf) |
157 (case String.fields (fn c => c = #"\n") input of |
158 | (line :: lines, rest) => |
158 [rest] => read (Buffer.add rest buf) x |
159 f (Buffer.content (Buffer.add line buf)) |
159 | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x))) |
160 #> fold f lines |
160 and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x |
161 #> read (Buffer.add rest Buffer.empty)); |
161 | read_lines (line :: more) x = read_lines more (f line x); |
162 in read Buffer.empty a end) path; |
162 in read Buffer.empty a end) path; |
163 |
163 |
164 val read = open_input TextIO.inputAll; |
164 val read = open_input TextIO.inputAll; |
165 |
165 |
166 |
166 |