author | wenzelm |
Wed, 08 Mar 2023 22:22:35 +0100 | |
changeset 77591 | 3f3dcf9f53f1 |
parent 74776 | 251bf0f2d5bb |
child 77692 | 3e746e684f4b |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62468
diff
changeset
|
1 |
(* Title: Pure/ML/ml_system.ML |
43948 | 2 |
Author: Makarius |
3 |
||
48416 | 4 |
ML system and platform operations. |
43948 | 5 |
*) |
6 |
||
7 |
signature ML_SYSTEM = |
|
8 |
sig |
|
9 |
val name: string |
|
10 |
val platform: string |
|
73586 | 11 |
val platform_is_linux: bool |
12 |
val platform_is_macos: bool |
|
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
48416
diff
changeset
|
13 |
val platform_is_windows: bool |
73586 | 14 |
val platform_is_unix: bool |
69701 | 15 |
val platform_is_64: bool |
72535 | 16 |
val platform_is_arm: bool |
62468 | 17 |
val platform_path: string -> string |
18 |
val standard_path: string -> string |
|
43948 | 19 |
end; |
20 |
||
21 |
structure ML_System: ML_SYSTEM = |
|
22 |
struct |
|
23 |
||
24 |
val SOME name = OS.Process.getEnv "ML_SYSTEM"; |
|
25 |
val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
|
73586 | 26 |
|
27 |
val platform_is_linux = String.isSuffix "linux" platform; |
|
28 |
val platform_is_macos = String.isSuffix "darwin" platform; |
|
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
48416
diff
changeset
|
29 |
val platform_is_windows = String.isSuffix "windows" platform; |
73586 | 30 |
val platform_is_unix = platform_is_linux orelse platform_is_macos; |
74776 | 31 |
val platform_is_64 = String.isPrefix "x86_64-" platform orelse String.isPrefix "arm64-" platform; |
32 |
val platform_is_arm = String.isPrefix "arm64_32-" platform orelse String.isPrefix "arm64-" platform; |
|
43948 | 33 |
|
62468 | 34 |
val platform_path = |
35 |
if platform_is_windows then |
|
36 |
fn path => |
|
37 |
if String.isPrefix "/" path andalso not (String.isPrefix "//" path) then |
|
38 |
(case String.tokens (fn c => c = #"/") path of |
|
39 |
"cygdrive" :: drive :: arcs => |
|
40 |
let |
|
41 |
val vol = |
|
42 |
(case Char.fromString drive of |
|
43 |
NONE => drive ^ ":" |
|
44 |
| SOME d => String.str (Char.toUpper d) ^ ":"); |
|
45 |
in String.concatWith "\\" (vol :: arcs) end |
|
46 |
| arcs => |
|
47 |
(case OS.Process.getEnv "CYGWIN_ROOT" of |
|
48 |
SOME root => OS.Path.concat (root, String.concatWith "\\" arcs) |
|
49 |
| NONE => raise Fail "Unknown environment variable CYGWIN_ROOT")) |
|
50 |
else String.translate (fn #"/" => "\\" | c => String.str c) path |
|
51 |
else fn path => path; |
|
52 |
||
53 |
val standard_path = |
|
54 |
if platform_is_windows then |
|
55 |
fn path => |
|
56 |
let |
|
57 |
val {vol, arcs, isAbs} = OS.Path.fromString path; |
|
58 |
val path' = String.translate (fn #"\\" => "/" | c => String.str c) path; |
|
59 |
in |
|
60 |
if isAbs then |
|
61 |
(case String.explode vol of |
|
62 |
[d, #":"] => |
|
63 |
String.concatWith "/" ("/cygdrive" :: String.str (Char.toLower d) :: arcs) |
|
64 |
| _ => path') |
|
65 |
else path' |
|
66 |
end |
|
67 |
else fn path => path; |
|
68 |
||
43948 | 69 |
end; |