equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/windows_path.ML |
|
2 Author: Makarius |
|
3 |
|
4 Windows file-system paths. |
|
5 *) |
|
6 |
|
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 String.concatWith "\\" (vol :: arcs) end |
|
17 | arcs => |
|
18 (case OS.Process.getEnv "CYGWIN_ROOT" of |
|
19 SOME root => OS.Path.concat (root, String.concatWith "\\" arcs) |
|
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; |
|