equal
deleted
inserted
replaced
161 |
161 |
162 |
162 |
163 (* base element *) |
163 (* base element *) |
164 |
164 |
165 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |
165 fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) |
166 | split_path _ path = error ("Cannot split path into dir/base: " ^ quote (implode_path path)); |
166 | split_path _ path = error ("Cannot split path into dir/base: " ^ print path); |
167 |
167 |
168 val dir = split_path #1; |
168 val dir = split_path #1; |
169 val base = split_path (fn (_, s) => Path [Basic s]); |
169 val base = split_path (fn (_, s) => Path [Basic s]); |
170 |
170 |
171 fun ext "" = I |
171 fun ext "" = I |