equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/ml_system.ML |
1 (* Title: Pure/ML-Systems/ml_system.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 ML system and platform information. |
4 ML system and platform operations. |
5 *) |
5 *) |
6 |
6 |
7 signature ML_SYSTEM = |
7 signature ML_SYSTEM = |
8 sig |
8 sig |
9 val name: string |
9 val name: string |
10 val is_polyml: bool |
10 val is_polyml: bool |
11 val is_smlnj: bool |
11 val is_smlnj: bool |
12 val platform: string |
12 val platform: string |
13 val platform_is_cygwin: bool |
13 val platform_is_cygwin: bool |
|
14 val share_common_data: unit -> unit |
|
15 val save_state: string -> unit |
14 end; |
16 end; |
15 |
17 |
16 structure ML_System: ML_SYSTEM = |
18 structure ML_System: ML_SYSTEM = |
17 struct |
19 struct |
18 |
20 |
21 val is_smlnj = String.isPrefix "smlnj" name; |
23 val is_smlnj = String.isPrefix "smlnj" name; |
22 |
24 |
23 val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
25 val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
24 val platform_is_cygwin = String.isSuffix "cygwin" platform; |
26 val platform_is_cygwin = String.isSuffix "cygwin" platform; |
25 |
27 |
|
28 fun share_common_data () = (); |
|
29 fun save_state _ = raise Fail "Cannot save state -- undefined operation"; |
|
30 |
26 end; |
31 end; |
27 |
32 |