22 val append: T -> T -> T |
22 val append: T -> T -> T |
23 val appends: T list -> T |
23 val appends: T list -> T |
24 val make: string list -> T |
24 val make: string list -> T |
25 val pack: T -> string |
25 val pack: T -> string |
26 val unpack: string -> T |
26 val unpack: string -> T |
|
27 val dir: T -> T |
27 val base: T -> T |
28 val base: T -> T |
28 val ext: string -> T -> T |
29 val ext: string -> T -> T |
29 val drop_ext: T -> T |
30 val split_ext: T -> T * string |
30 val dir: T -> T |
|
31 val expand: T -> T |
31 val expand: T -> T |
32 val position: T -> Position.T |
32 val position: T -> Position.T |
33 end; |
33 end; |
34 |
34 |
35 structure Path: PATH = |
35 structure Path: PATH = |
132 fun split_path f (path as Path xs) = |
132 fun split_path f (path as Path xs) = |
133 (case try split_last xs of |
133 (case try split_last xs of |
134 Some (prfx, Basic s) => f (prfx, s) |
134 Some (prfx, Basic s) => f (prfx, s) |
135 | _ => error ("Cannot split path into dir/base: " ^ quote (pack path))); |
135 | _ => error ("Cannot split path into dir/base: " ^ quote (pack path))); |
136 |
136 |
|
137 val dir = split_path (fn (prfx, _) => Path prfx); |
137 val base = split_path (fn (_, s) => Path [Basic s]); |
138 val base = split_path (fn (_, s) => Path [Basic s]); |
138 |
139 |
139 fun ext "" path = path |
140 fun ext "" path = path |
140 | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path; |
141 | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path; |
141 |
142 |
142 val drop_ext = split_path (fn (prfx, s) => append (Path prfx) |
143 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx)) |
143 (case take_suffix (not_equal ".") (explode s) of |
144 (case take_suffix (not_equal ".") (explode s) of |
144 ([], _) => Path [Basic s] |
145 ([], _) => (Path [Basic s], "") |
145 | (cs, _) => Path [Basic (implode (take (length cs - 1, cs)))])); |
146 | (cs, e) => (Path [Basic (implode (take (length cs - 1, cs)))], implode e))); |
146 |
|
147 val dir = split_path (fn (prfx, _) => Path prfx); |
|
148 |
147 |
149 |
148 |
150 (* evaluate variables *) |
149 (* evaluate variables *) |
151 |
150 |
152 fun eval env (Variable s) = rep (env s) |
151 fun eval env (Variable s) = rep (env s) |