equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/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 is_polyml: bool |
|
11 val is_smlnj: bool |
|
12 val platform: string |
|
13 val platform_is_windows: bool |
|
14 val share_common_data: unit -> unit |
|
15 val save_state: string -> unit |
|
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"; |
|
26 val platform_is_windows = String.isSuffix "windows" platform; |
|
27 |
|
28 fun share_common_data () = (); |
|
29 fun save_state _ = raise Fail "Cannot save state -- undefined operation"; |
|
30 |
|
31 end; |
|
32 |
|