equal
deleted
inserted
replaced
18 val is_absolute: T -> bool |
18 val is_absolute: T -> bool |
19 val is_basic: T -> bool |
19 val is_basic: T -> bool |
20 val append: T -> T -> T |
20 val append: T -> T -> T |
21 val appends: T list -> T |
21 val appends: T list -> T |
22 val make: string list -> T |
22 val make: string list -> T |
23 val print: T -> string |
|
24 val implode: T -> string |
23 val implode: T -> string |
25 val explode: string -> T |
24 val explode: string -> T |
|
25 val pretty: T -> Pretty.T |
|
26 val print: T -> string |
26 val dir: T -> 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 split_ext: T -> T * string |
30 val split_ext: T -> T * string |
30 val expand: T -> T |
31 val expand: T -> T |
117 fun implode_path (Path []) = "." |
118 fun implode_path (Path []) = "." |
118 | implode_path (Path [Root ""]) = "/" |
119 | implode_path (Path [Root ""]) = "/" |
119 | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); |
120 | implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); |
120 |
121 |
121 end; |
122 end; |
122 |
|
123 val print = quote o implode_path; |
|
124 |
123 |
125 |
124 |
126 (* explode *) |
125 (* explode *) |
127 |
126 |
128 local |
127 local |
150 in Path (norm (explode_elems raw_elems @ roots)) end; |
149 in Path (norm (explode_elems raw_elems @ roots)) end; |
151 |
150 |
152 end; |
151 end; |
153 |
152 |
154 |
153 |
|
154 (* print *) |
|
155 |
|
156 fun pretty path = |
|
157 let val s = implode_path path |
|
158 in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; |
|
159 |
|
160 val print = Pretty.str_of o pretty; |
|
161 |
|
162 |
155 (* base element *) |
163 (* base element *) |
156 |
164 |
157 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) |
158 | 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: " ^ quote (implode_path path)); |
159 |
167 |