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