23 val rm: Path.T -> unit |
23 val rm: Path.T -> unit |
24 val mkdir: Path.T -> unit |
24 val mkdir: Path.T -> unit |
25 val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a |
25 val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a |
26 val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a |
26 val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a |
27 val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a |
27 val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a |
|
28 val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
28 val read: Path.T -> string |
29 val read: Path.T -> string |
29 val write: Path.T -> string -> unit |
30 val write: Path.T -> string -> unit |
30 val append: Path.T -> string -> unit |
31 val append: Path.T -> string -> unit |
31 val write_list: Path.T -> string list -> unit |
32 val write_list: Path.T -> string list -> unit |
32 val append_list: Path.T -> string list -> unit |
33 val append_list: Path.T -> string list -> unit |
|
34 val write_buffer: Path.T -> Buffer.T -> unit |
33 val eq: Path.T * Path.T -> bool |
35 val eq: Path.T * Path.T -> bool |
34 val copy: Path.T -> Path.T -> unit |
36 val copy: Path.T -> Path.T -> unit |
35 val copy_dir: Path.T -> Path.T -> unit |
37 val copy_dir: Path.T -> Path.T -> unit |
36 end; |
38 end; |
37 |
39 |
124 |
126 |
125 fun is_dir path = |
127 fun is_dir path = |
126 the_default false (try OS.FileSys.isDir (platform_path path)); |
128 the_default false (try OS.FileSys.isDir (platform_path path)); |
127 |
129 |
128 |
130 |
129 (* read / write files *) |
131 (* open files *) |
130 |
132 |
131 local |
133 local |
132 |
134 |
133 fun with_file open_file close_file f path = |
135 fun with_file open_file close_file f path = |
134 let val file = open_file path |
136 let val file = open_file path |
135 in Exn.release (Exn.capture f file before close_file file) end; |
137 in Exn.release (Exn.capture f file before close_file file) end; |
136 |
138 |
137 fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts; |
|
138 |
|
139 in |
139 in |
140 |
140 |
141 fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path; |
141 fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path; |
142 fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path; |
142 fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path; |
143 fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path; |
143 fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path; |
144 |
144 |
|
145 end; |
|
146 |
|
147 |
|
148 (* input *) |
|
149 |
|
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 => |
|
152 let |
|
153 val first_line = first_field "\n"; |
|
154 fun split str x = |
|
155 (case first_line str of |
|
156 SOME (line, rest) => split rest (f line x) |
|
157 | NONE => read (Buffer.add str Buffer.empty) x) |
|
158 and read buf x = |
|
159 let val str = TextIO.input file in |
|
160 (case first_line str of |
|
161 SOME (line, rest) => split rest (f (Buffer.content (Buffer.add line buf)) x) |
|
162 | NONE => |
|
163 if str = "" then (case Buffer.content buf of "" => x | line => f line x) |
|
164 else read (Buffer.add str buf) x) |
|
165 end; |
|
166 in read Buffer.empty a end) path; |
|
167 |
145 val read = open_input TextIO.inputAll; |
168 val read = open_input TextIO.inputAll; |
|
169 |
|
170 |
|
171 (* output *) |
|
172 |
|
173 fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts; |
146 |
174 |
147 fun write_list path txts = open_output (output txts) path; |
175 fun write_list path txts = open_output (output txts) path; |
148 fun append_list path txts = open_append (output txts) path; |
176 fun append_list path txts = open_append (output txts) path; |
149 |
177 |
150 fun write path txt = write_list path [txt]; |
178 fun write path txt = write_list path [txt]; |
151 fun append path txt = append_list path [txt]; |
179 fun append path txt = append_list path [txt]; |
152 |
180 |
153 end; |
181 fun write_buffer path buf = open_output (Buffer.output buf) path; |
|
182 |
|
183 |
|
184 (* copy *) |
154 |
185 |
155 fun eq paths = |
186 fun eq paths = |
156 (case try (pairself (OS.FileSys.fileId o platform_path)) paths of |
187 (case try (pairself (OS.FileSys.fileId o platform_path)) paths of |
157 SOME ids => is_equal (OS.FileSys.compare ids) |
188 SOME ids => is_equal (OS.FileSys.compare ids) |
158 | NONE => false); |
189 | NONE => false); |