1 (* Title: Pure/RAW/ml_system.ML |
|
2 Author: Makarius |
|
3 |
|
4 ML system and platform operations. |
|
5 *) |
|
6 |
|
7 signature ML_SYSTEM = |
|
8 sig |
|
9 val name: string |
|
10 val platform: string |
|
11 val platform_is_windows: bool |
|
12 val platform_path: string -> string |
|
13 val standard_path: string -> string |
|
14 end; |
|
15 |
|
16 structure ML_System: ML_SYSTEM = |
|
17 struct |
|
18 |
|
19 val SOME name = OS.Process.getEnv "ML_SYSTEM"; |
|
20 val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
|
21 val platform_is_windows = String.isSuffix "windows" platform; |
|
22 |
|
23 val platform_path = |
|
24 if platform_is_windows then |
|
25 fn path => |
|
26 if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then |
|
27 (case String.tokens (fn c => c = #"/") path of |
|
28 "cygdrive" :: drive :: arcs => |
|
29 let |
|
30 val vol = |
|
31 (case Char.fromString drive of |
|
32 NONE => drive ^ ":" |
|
33 | SOME d => String.str (Char.toUpper d) ^ ":"); |
|
34 in String.concatWith "\\" (vol :: arcs) end |
|
35 | arcs => |
|
36 (case OS.Process.getEnv "CYGWIN_ROOT" of |
|
37 SOME root => OS.Path.concat (root, String.concatWith "\\" arcs) |
|
38 | NONE => raise Fail "Unknown environment variable CYGWIN_ROOT")) |
|
39 else String.translate (fn #"/" => "\\" | c => String.str c) path |
|
40 else fn path => path; |
|
41 |
|
42 val standard_path = |
|
43 if platform_is_windows then |
|
44 fn path => |
|
45 let |
|
46 val {vol, arcs, isAbs} = OS.Path.fromString path; |
|
47 val path' = String.translate (fn #"\\" => "/" | c => String.str c) path; |
|
48 in |
|
49 if isAbs then |
|
50 (case String.explode vol of |
|
51 [d, #":"] => |
|
52 String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs) |
|
53 | _ => path') |
|
54 else path' |
|
55 end |
|
56 else fn path => path; |
|
57 |
|
58 end; |
|