| 190 |
end) |
end) |
| 191 |
end |
end |
| 192 |
|
|
| 193 |
fun joinDirFile { dir as (CUR _ | CONFIG_ANCHOR _), file } = |
(* . and .. are not permitted as file parameter *) |
| 194 |
fresh (dir, file) |
fun joinDirFile { dir, file } = |
| 195 |
| joinDirFile { dir = SPEC { context, spec, ... }, file } = let |
if file = P.currentArc orelse file = P.parentArc then |
| 196 |
val j = |
raise Fail "AbsPath.joinDirFile: . or .." |
| 197 |
P.mkCanonical (P.joinDirFile { dir = spec, file = file }) |
else case dir of |
| 198 |
in |
(CUR _ | CONFIG_ANCHOR _) => fresh (dir, file) |
| 199 |
fresh (context, j) |
| SPEC { context, spec, ... } => |
| 200 |
end |
fresh (context, P.joinDirFile { dir = spec, file = file }) |
| 201 |
|
|
| 202 |
(* The cases where we try to split CUR, CONFIG_ANCHOR, ".", |
(* splitDirFile never walks past a context. |
| 203 |
* or any path ending in ".." should never occur in practice. |
* Moreover, it is an error to split something that ends in "..". *) |
|
* It would perhaps be better to put error-handling here... *) |
|
| 204 |
fun splitDirFile (x as (CUR _ | CONFIG_ANCHOR _)) = |
fun splitDirFile (x as (CUR _ | CONFIG_ANCHOR _)) = |
| 205 |
{ dir = x, file = P.currentArc } |
raise Fail "AbsPath.splitDirFile: CUR or CONFIG_ANCHOR" |
| 206 |
| splitDirFile (SPEC { context, spec, ... }) = let |
| splitDirFile (SPEC { context, spec, ... }) = let |
| 207 |
|
fun loop "" = |
| 208 |
|
raise Fail "AbsPath.splitDirFile: tried to split context" |
| 209 |
|
| loop spec = let |
| 210 |
val { dir, file } = P.splitDirFile spec |
val { dir, file } = P.splitDirFile spec |
|
val dir = if dir = "" then P.currentArc else dir |
|
| 211 |
in |
in |
| 212 |
{ dir = fresh (context, dir), file = file } |
if file = P.currentArc then loop dir |
| 213 |
|
else if file = P.parentArc then |
| 214 |
|
raise Fail "AbsPath.splitDirFile: <path>/.." |
| 215 |
|
else (dir, file) |
| 216 |
|
end |
| 217 |
|
val (dir, file) = loop spec |
| 218 |
|
val dir = if dir = "" then context else fresh (context, dir) |
| 219 |
|
in |
| 220 |
|
{ dir = dir, file = file } |
| 221 |
end |
end |
| 222 |
|
|
| 223 |
val dir = #dir o splitDirFile |
val dir = #dir o splitDirFile |
Parent Directory
| 
Revision Log
| 
Patch
