18 val rm: Path.T -> unit |
18 val rm: Path.T -> unit |
19 val is_dir: Path.T -> bool |
19 val is_dir: Path.T -> bool |
20 val is_file: Path.T -> bool |
20 val is_file: Path.T -> bool |
21 val check_dir: Path.T -> Path.T |
21 val check_dir: Path.T -> Path.T |
22 val check_file: Path.T -> Path.T |
22 val check_file: Path.T -> Path.T |
23 val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a |
|
24 val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a |
|
25 val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a |
|
26 val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a |
|
27 val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
23 val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
28 val read_dir: Path.T -> string list |
24 val read_dir: Path.T -> string list |
29 val input: BinIO.instream -> string |
|
30 val input_size: int -> BinIO.instream -> string |
|
31 val input_all: BinIO.instream -> string |
|
32 val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
25 val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a |
33 val read_lines: Path.T -> string list |
26 val read_lines: Path.T -> string list |
34 val read: Path.T -> string |
27 val read: Path.T -> string |
35 val write: Path.T -> string -> unit |
28 val write: Path.T -> string -> unit |
36 val append: Path.T -> string -> unit |
29 val append: Path.T -> string -> unit |
37 val output: BinIO.outstream -> string -> unit |
|
38 val outputs: BinIO.outstream -> string list -> unit |
|
39 val write_list: Path.T -> string list -> unit |
30 val write_list: Path.T -> string list -> unit |
40 val append_list: Path.T -> string list -> unit |
31 val append_list: Path.T -> string list -> unit |
41 val eq: Path.T * Path.T -> bool |
32 val eq: Path.T * Path.T -> bool |
42 end; |
33 end; |
43 |
34 |
91 fun check_file path = |
82 fun check_file path = |
92 if is_file path then path |
83 if is_file path then path |
93 else error ("No such file: " ^ Path.print (Path.expand path)); |
84 else error ("No such file: " ^ Path.print (Path.expand path)); |
94 |
85 |
95 |
86 |
96 (* open streams *) |
|
97 |
|
98 local |
|
99 |
|
100 fun with_file open_file close_file f = |
|
101 Thread_Attributes.uninterruptible (fn restore_attributes => fn path => |
|
102 let |
|
103 val file = open_file path; |
|
104 val result = Exn.capture (restore_attributes f) file; |
|
105 in close_file file; Exn.release result end); |
|
106 |
|
107 in |
|
108 |
|
109 fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; |
|
110 fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; |
|
111 fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; |
|
112 fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; |
|
113 |
|
114 end; |
|
115 |
|
116 |
|
117 (* directory content *) |
87 (* directory content *) |
118 |
88 |
119 fun fold_dir f path a = |
89 fun fold_dir f path a = |
120 check_dir path |> open_dir (fn stream => |
90 check_dir path |> File_Stream.open_dir (fn stream => |
121 let |
91 let |
122 fun read x = |
92 fun read x = |
123 (case OS.FileSys.readDir stream of |
93 (case OS.FileSys.readDir stream of |
124 NONE => x |
94 NONE => x |
125 | SOME entry => read (f entry x)); |
95 | SOME entry => read (f entry x)); |
126 in read a end); |
96 in read a end); |
127 |
97 |
128 fun read_dir path = sort_strings (fold_dir cons path []); |
98 fun read_dir path = sort_strings (fold_dir cons path []); |
129 |
99 |
130 |
100 |
131 (* input *) |
|
132 |
|
133 val input = Byte.bytesToString o BinIO.input; |
|
134 fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n)); |
|
135 val input_all = Byte.bytesToString o BinIO.inputAll; |
|
136 |
|
137 (* |
101 (* |
138 scalable iterator: |
102 scalable iterator: |
139 . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine |
103 . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine |
140 . optional terminator at end-of-input |
104 . optional terminator at end-of-input |
141 *) |
105 *) |
142 fun fold_lines f path a = open_input (fn file => |
106 fun fold_lines f path a = File_Stream.open_input (fn file => |
143 let |
107 let |
144 fun read buf x = |
108 fun read buf x = |
145 (case input file of |
109 (case File_Stream.input file of |
146 "" => (case Buffer.content buf of "" => x | line => f line x) |
110 "" => (case Buffer.content buf of "" => x | line => f line x) |
147 | input => |
111 | input => |
148 (case String.fields (fn c => c = #"\n") input of |
112 (case String.fields (fn c => c = #"\n") input of |
149 [rest] => read (Buffer.add rest buf) x |
113 [rest] => read (Buffer.add rest buf) x |
150 | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x))) |
114 | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x))) |
152 | read_more (line :: more) x = read_more more (f line x); |
116 | read_more (line :: more) x = read_more more (f line x); |
153 in read Buffer.empty a end) path; |
117 in read Buffer.empty a end) path; |
154 |
118 |
155 fun read_lines path = rev (fold_lines cons path []); |
119 fun read_lines path = rev (fold_lines cons path []); |
156 |
120 |
157 val read = open_input input_all; |
121 val read = File_Stream.open_input File_Stream.input_all; |
158 |
122 |
159 |
123 |
160 (* output *) |
124 (* write *) |
161 |
125 |
162 fun output file txt = BinIO.output (file, Byte.stringToBytes txt); |
126 fun write_list path ss = File_Stream.open_output (fn stream => File_Stream.outputs stream ss) path; |
163 val outputs = List.app o output; |
127 fun append_list path ss = File_Stream.open_append (fn stream => File_Stream.outputs stream ss) path; |
164 |
|
165 fun output_list txts file = List.app (output file) txts; |
|
166 fun write_list path txts = open_output (output_list txts) path; |
|
167 fun append_list path txts = open_append (output_list txts) path; |
|
168 |
128 |
169 fun write path txt = write_list path [txt]; |
129 fun write path txt = write_list path [txt]; |
170 fun append path txt = append_list path [txt]; |
130 fun append path txt = append_list path [txt]; |
171 |
131 |
172 |
132 |