author | wenzelm |
Thu, 20 Aug 2015 21:14:58 +0200 | |
changeset 60993 | 531a48ae1425 |
parent 60970 | src/Pure/ML-Systems/windows_polyml.ML@e08d868ceca9 |
child 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) ^ ":"); |
|
16 |
in OS.Path.toString {vol = vol, arcs = arcs, isAbs = true} end |
|
17 |
| arcs => |
|
18 |
(case OS.Process.getEnv "CYGWIN_ROOT" of |
|
19 |
SOME root => |
|
20 |
OS.Path.concat (root, OS.Path.toString {vol = "", arcs = arcs, isAbs = false}) |
|
21 |
| NONE => raise Fail "Unknown environment variable CYGWIN_ROOT")) |
|
22 |
else String.translate (fn #"/" => "\\" | c => String.str c) path; |
|
23 |
||
24 |
fun ml_standard_path path = |
|
25 |
let |
|
26 |
val {vol, arcs, isAbs} = OS.Path.fromString path; |
|
27 |
val path' = String.translate (fn #"\\" => "/" | c => String.str c) path; |
|
28 |
in |
|
29 |
if isAbs then |
|
30 |
(case String.explode vol of |
|
31 |
[d, #":"] => |
|
32 |
String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs) |
|
33 |
| _ => path') |
|
34 |
else path' |
|
35 |
end; |