equal
deleted
inserted
replaced
137 | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path; |
137 | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path; |
138 |
138 |
139 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx)) |
139 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx)) |
140 (case take_suffix (fn c => c <> ".") (explode s) of |
140 (case take_suffix (fn c => c <> ".") (explode s) of |
141 ([], _) => (Path [Basic s], "") |
141 ([], _) => (Path [Basic s], "") |
142 | (cs, e) => (Path [Basic (implode ((uncurry take) (length cs - 1, cs)))], implode e))); |
142 | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e))); |
143 |
143 |
144 |
144 |
145 (* expand variables *) |
145 (* expand variables *) |
146 |
146 |
147 fun eval (Variable s) = |
147 fun eval (Variable s) = |