author | wenzelm |
Thu, 17 Dec 2015 17:32:01 +0100 | |
changeset 61862 | e2a9e46ac0fb |
parent 61137 | 4010e1559a24 |
permissions | -rw-r--r-- |
60993 | 1 |
(* Title: Pure/ML-Systems/windows_path.ML |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
3 |
|
60993 | 4 |
Windows file-system paths. |
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
diff
changeset
|
5 |
*) |
60963
3c6751e2f10a
more setup for native Windows (Pure and HOL session with image);
wenzelm
parents:
60962
diff
changeset
|
6 |
|
60965 | 7 |
fun ml_platform_path path = |
8 |
if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then |
|
9 |
(case String.tokens (fn c => c = #"/") path of |
|
10 |
"cygdrive" :: drive :: arcs => |
|
11 |
let |
|
12 |
val vol = |
|
13 |
(case Char.fromString drive of |
|
14 |
NONE => drive ^ ":" |
|
15 |
| SOME d => String.str (Char.toUpper d) ^ ":"); |
|
61137
4010e1559a24
more basic Windows path operations -- evade exception InvalidArc with Unicode;
wenzelm
parents:
60993
diff
changeset
|
16 |
in String.concatWith "\\" (vol :: arcs) end |
60965 | 17 |
| arcs => |
18 |
(case OS.Process.getEnv "CYGWIN_ROOT" of |
|
61137
4010e1559a24
more basic Windows path operations -- evade exception InvalidArc with Unicode;
wenzelm
parents:
60993
diff
changeset
|
19 |
SOME root => OS.Path.concat (root, String.concatWith "\\" arcs) |
60965 | 20 |
| NONE => raise Fail "Unknown environment variable CYGWIN_ROOT")) |
21 |
else String.translate (fn #"/" => "\\" | c => String.str c) path; |
|
22 |
||
23 |
fun ml_standard_path path = |
|
24 |
let |
|
25 |
val {vol, arcs, isAbs} = OS.Path.fromString path; |
|
26 |
val path' = String.translate (fn #"\\" => "/" | c => String.str c) path; |
|
27 |
in |
|
28 |
if isAbs then |
|
29 |
(case String.explode vol of |
|
30 |
[d, #":"] => |
|
31 |
String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs) |
|
32 |
| _ => path') |
|
33 |
else path' |
|
34 |
end; |