34 |
val native : { context: context, spec: string } -> t |
val native : { context: context, spec: string } -> t |
35 |
val standard : PathConfig.mode -> { context: context, spec: string } -> t |
val standard : PathConfig.mode -> { context: context, spec: string } -> t |
36 |
|
|
37 |
|
val fromDescr : PathConfig.mode -> string -> t |
38 |
|
|
39 |
(* the second path argument is the path of the group spec that |
(* the second path argument is the path of the group spec that |
40 |
* pickling is based upon. *) |
* pickling is based upon. *) |
41 |
val pickle : (bool -> unit) -> t * t -> string list |
val pickle : (bool -> unit) -> t * t -> string list |
103 |
cache: elaboration option ref, |
cache: elaboration option ref, |
104 |
config_name: string } |
config_name: string } |
105 |
| DIR_OF of t |
| DIR_OF of t |
106 |
| ROOT |
| ROOT of string (* carries volume *) |
107 |
|
|
108 |
and t = |
and t = |
109 |
PATH of { context: context, |
PATH of { context: context, |
167 |
| validElab (SOME (e as { stamp, name, id })) = |
| validElab (SOME (e as { stamp, name, id })) = |
168 |
if Era.isThisEra stamp then SOME e else NONE |
if Era.isThisEra stamp then SOME e else NONE |
169 |
|
|
170 |
val rootName = P.toString { isAbs = true, arcs = [], vol = "" } |
fun rootName vol = P.toString { isAbs = true, arcs = [], vol = vol } |
171 |
val rootId = ref (NONE: id option) |
val rootId = let |
172 |
|
val m = ref (StringMap.empty: id option ref StringMap.map) |
173 |
|
in |
174 |
|
fn vol => |
175 |
|
(case StringMap.find (!m, vol) of |
176 |
|
NONE => let |
177 |
|
val idr = ref NONE |
178 |
|
in |
179 |
|
m := StringMap.insert (!m, vol, idr); |
180 |
|
idr |
181 |
|
end |
182 |
|
| SOME idr => idr) |
183 |
|
end |
184 |
|
|
185 |
fun elabContext c = |
fun elabContext c = |
186 |
case c of |
case c of |
197 |
in |
in |
198 |
{ name = P.dir name, stamp = stamp, id = ref NONE } |
{ name = P.dir name, stamp = stamp, id = ref NONE } |
199 |
end |
end |
200 |
| ROOT => { stamp = Era.thisEra (), |
| ROOT vol => { stamp = Era.thisEra (), |
201 |
name = rootName, id = rootId } |
name = rootName vol, |
202 |
|
id = rootId vol } |
203 |
|
|
204 |
and elab (PATH { context, spec, cache }) = |
and elab (PATH { context, spec, cache }) = |
205 |
case validElab (!cache) of |
case validElab (!cache) of |
239 |
(* make an abstract path from a native string *) |
(* make an abstract path from a native string *) |
240 |
fun native { spec, context } = let |
fun native { spec, context } = let |
241 |
val { isAbs, vol, arcs } = P.fromString spec |
val { isAbs, vol, arcs } = P.fromString spec |
242 |
val relSpec = P.toString { isAbs = false, vol = vol, arcs = arcs } |
val relSpec = P.toString { isAbs = false, vol = "", arcs = arcs } |
243 |
in |
in |
244 |
if isAbs then fresh (ROOT, relSpec) |
if isAbs then fresh (ROOT vol, relSpec) |
245 |
else fresh (context, relSpec) |
else fresh (context, relSpec) |
246 |
end |
end |
247 |
|
|
262 |
in |
in |
263 |
case String.fields delim spec of |
case String.fields delim spec of |
264 |
[""] => impossible "AbsPath.standard: zero-length name" |
[""] => impossible "AbsPath.standard: zero-length name" |
265 |
| "" :: arcs => mk (arcs, ROOT) |
| "" :: arcs => mk (arcs, ROOT "") |
266 |
| [] => impossible "AbsPath.standard: no fields" |
| [] => impossible "AbsPath.standard: no fields" |
267 |
| arcs as (arc1 :: _) => |
| arcs as (arc1 :: _) => |
268 |
(case PathConfig.configAnchor mode arc1 of |
(case PathConfig.configAnchor mode arc1 of |
281 |
fun pickle warn (path, gpath) = let |
fun pickle warn (path, gpath) = let |
282 |
fun p_p (PATH { spec, context, ... }) = |
fun p_p (PATH { spec, context, ... }) = |
283 |
spec :: p_c context |
spec :: p_c context |
284 |
and p_c ROOT = (warn true; ["r"]) |
and p_c (ROOT vol) = (warn true; [vol, "r"]) |
285 |
| p_c (THEN_CWD _) = impossible "AbsPath.pickle: THEN_CWD" |
| p_c (THEN_CWD _) = impossible "AbsPath.pickle: THEN_CWD" |
286 |
| p_c (CONFIG_ANCHOR { config_name = n, ... }) = [n, "a"] |
| p_c (CONFIG_ANCHOR { config_name = n, ... }) = [n, "a"] |
287 |
| p_c (DIR_OF p) = |
| p_c (DIR_OF p) = |
295 |
fun u_p (s :: l) = |
fun u_p (s :: l) = |
296 |
PATH { spec = s, context = u_c l, cache = ref NONE } |
PATH { spec = s, context = u_c l, cache = ref NONE } |
297 |
| u_p [] = raise Format |
| u_p [] = raise Format |
298 |
and u_c ["r"] = ROOT |
and u_c [vol, "r"] = ROOT vol |
299 |
| u_c ["c"] = DIR_OF gpath |
| u_c ["c"] = DIR_OF gpath |
300 |
| u_c [n, "a"] = |
| u_c [n, "a"] = |
301 |
(case PathConfig.configAnchor mode n of |
(case PathConfig.configAnchor mode n of |
321 |
| d_c (DIR_OF (PATH { spec, context, ... }), l) = |
| d_c (DIR_OF (PATH { spec, context, ... }), l) = |
322 |
d_c (context, dir (spec, l)) |
d_c (context, dir (spec, l)) |
323 |
| d_c (THEN_CWD _, l) = "./" :: l |
| d_c (THEN_CWD _, l) = "./" :: l |
324 |
| d_c (ROOT, l) = "/" :: l |
| d_c (ROOT "", l) = "/" :: l |
325 |
|
| d_c (ROOT vol, l) = "%" :: vol :: "/" :: l |
326 |
in |
in |
327 |
concat (d_c (context, [spec])) |
concat (d_c (context, [spec])) |
328 |
end |
end |
329 |
|
|
330 |
|
fun fromDescr mode "" = fresh (cwdContext (), P.currentArc) |
331 |
|
| fromDescr mode d = let |
332 |
|
val l = size d |
333 |
|
fun split n = |
334 |
|
if n >= l then |
335 |
|
(String.substring (d, 1, l), P.currentArc) |
336 |
|
else if String.sub (d, n) = #"/" then |
337 |
|
(String.substring (d, 1, n - 1), |
338 |
|
String.extract (d, n + 1, NONE)) |
339 |
|
else split (n + 1) |
340 |
|
in |
341 |
|
case String.sub (d, 0) of |
342 |
|
#"$" => let |
343 |
|
val (a, s) = split 1 |
344 |
|
in |
345 |
|
case PathConfig.configAnchor mode a of |
346 |
|
NONE => raise BadAnchor a |
347 |
|
| SOME fetch => |
348 |
|
fresh (CONFIG_ANCHOR { config_name = a, |
349 |
|
fetch = fetch, |
350 |
|
cache = ref NONE }, |
351 |
|
s) |
352 |
|
end |
353 |
|
| #"/" => fresh (ROOT "", String.extract (d, 1, NONE)) |
354 |
|
| #"." => fresh (cwdContext (), String.extract (d, 2, NONE)) |
355 |
|
| #"%" => let |
356 |
|
val (v, s) = split 1 |
357 |
|
in |
358 |
|
fresh (ROOT v, s) |
359 |
|
end |
360 |
|
| _ => fresh (cwdContext (), d) |
361 |
|
end |
362 |
|
|
363 |
fun reAnchoredName (p, dirstring) = let |
fun reAnchoredName (p, dirstring) = let |
364 |
fun path (PATH { context, spec, ... }) = let |
fun path (PATH { context, spec, ... }) = let |
365 |
fun mk c = P.concat (c, spec) |
fun mk c = P.concat (c, spec) |
369 |
and ctxt (CONFIG_ANCHOR { config_name = n, ... }) = |
and ctxt (CONFIG_ANCHOR { config_name = n, ... }) = |
370 |
SOME (P.concat (dirstring, n)) |
SOME (P.concat (dirstring, n)) |
371 |
| ctxt (DIR_OF p) = Option.map P.dir (path p) |
| ctxt (DIR_OF p) = Option.map P.dir (path p) |
372 |
| ctxt (THEN_CWD _) = (Say.say ["."]; NONE) |
| ctxt (THEN_CWD _) = NONE |
373 |
| ctxt ROOT = (Say.say ["/"]; NONE) |
| ctxt (ROOT _) = NONE |
374 |
in |
in |
375 |
path p |
path p |
376 |
end |
end |