author | wenzelm |
Thu, 20 Aug 2015 19:19:19 +0200 | |
changeset 60989 | c967d423953a |
parent 60962 | faa452d8e265 |
permissions | -rw-r--r-- |
43948 | 1 |
(* Title: Pure/ML-Systems/ml_system.ML |
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 is_polyml: bool |
|
11 |
val is_smlnj: bool |
|
12 |
val platform: string |
|
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
48416
diff
changeset
|
13 |
val platform_is_windows: bool |
48416 | 14 |
val share_common_data: unit -> unit |
15 |
val save_state: string -> unit |
|
43948 | 16 |
end; |
17 |
||
18 |
structure ML_System: ML_SYSTEM = |
|
19 |
struct |
|
20 |
||
21 |
val SOME name = OS.Process.getEnv "ML_SYSTEM"; |
|
22 |
val is_polyml = String.isPrefix "polyml" name; |
|
23 |
val is_smlnj = String.isPrefix "smlnj" name; |
|
24 |
||
25 |
val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
|
60962
faa452d8e265
basic setup for native Windows (RAW session without image);
wenzelm
parents:
48416
diff
changeset
|
26 |
val platform_is_windows = String.isSuffix "windows" platform; |
43948 | 27 |
|
48416 | 28 |
fun share_common_data () = (); |
29 |
fun save_state _ = raise Fail "Cannot save state -- undefined operation"; |
|
30 |
||
43948 | 31 |
end; |
32 |