1(*  Title:      Pure/ML/ml_system.ML
2    Author:     Makarius
3
4ML system and platform operations.
5*)
6
7signature ML_SYSTEM =
8sig
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
14end;
15
16structure ML_System: ML_SYSTEM =
17struct
18
19val SOME name = OS.Process.getEnv "ML_SYSTEM";
20val SOME platform = OS.Process.getEnv "ML_PLATFORM";
21val platform_is_windows = String.isSuffix "windows" platform;
22
23val 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
42val 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
58end;
59