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