376 |
|
|
377 |
fun cwd () = (revalidateCwd (); CWD (!cwd_info)) |
fun cwd () = (revalidateCwd (); CWD (!cwd_info)) |
378 |
|
|
379 |
val osstring = pp2name o #pp o elab_file o unintern |
val osstring = I.canonical o pp2name o #pp o elab_file o unintern |
380 |
|
|
381 |
fun osstring_prefile { context, arcs, err } = |
fun osstring_prefile { context, arcs, err } = |
382 |
pp2name (#pp (augElab arcs (elab_dir context))) |
I.canonical (pp2name (#pp (augElab arcs (elab_dir context)))) |
383 |
|
|
384 |
val descr = encode0 true o pre |
val descr = encode0 true o pre |
385 |
|
|
386 |
fun osstring_dir d = |
fun osstring_dir d = |
387 |
case pp2name (#pp (elab_dir d)) of |
case pp2name (#pp (elab_dir d)) of |
388 |
"" => P.currentArc |
"" => P.currentArc |
389 |
| s => s |
| s => I.canonical s |
390 |
|
|
391 |
fun osstring' f = let |
fun osstring' f = let |
392 |
val oss = osstring f |
val oss = osstring f |
548 |
{ context = context, arcs = arcs @ morearcs, err = err } |
{ context = context, arcs = arcs @ morearcs, err = err } |
549 |
|
|
550 |
fun osstring_reanchored cvt f = |
fun osstring_reanchored cvt f = |
551 |
Option.map pp2name (#reanchor (elab_file (unintern f)) cvt) |
Option.map (I.canonical o pp2name) |
552 |
|
(#reanchor (elab_file (unintern f)) cvt) |
553 |
|
|
554 |
fun osstring_prefile_relative (p as { arcs, context, ... }) = |
fun osstring_prefile_relative (p as { arcs, context, ... }) = |
555 |
case context of |
case context of |
556 |
DIR _ => P.toString { arcs = arcs, vol = "", isAbs = false } |
DIR _ => I.canonical |
557 |
|
(P.toString { arcs = arcs, vol = "", isAbs = false }) |
558 |
| _ => osstring_prefile p |
| _ => osstring_prefile p |
559 |
|
|
560 |
val osstring_relative = osstring_prefile_relative o pre |
val osstring_relative = osstring_prefile_relative o pre |