src/Pure/ML/ml_system.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62508 d0b68218ea55
child 69701 b5ecabcfb780
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/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;