equal
deleted
inserted
replaced
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 platform_is_windows: bool |
14 val share_common_data: unit -> unit |
15 val share_common_data: unit -> unit |
15 val save_state: string -> unit |
16 val save_state: string -> unit |
16 end; |
17 end; |
17 |
18 |
18 structure ML_System: ML_SYSTEM = |
19 structure ML_System: ML_SYSTEM = |
22 val is_polyml = String.isPrefix "polyml" name; |
23 val is_polyml = String.isPrefix "polyml" name; |
23 val is_smlnj = String.isPrefix "smlnj" name; |
24 val is_smlnj = String.isPrefix "smlnj" name; |
24 |
25 |
25 val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
26 val SOME platform = OS.Process.getEnv "ML_PLATFORM"; |
26 val platform_is_cygwin = String.isSuffix "cygwin" platform; |
27 val platform_is_cygwin = String.isSuffix "cygwin" platform; |
|
28 val platform_is_windows = String.isSuffix "windows" platform; |
27 |
29 |
28 fun share_common_data () = (); |
30 fun share_common_data () = (); |
29 fun save_state _ = raise Fail "Cannot save state -- undefined operation"; |
31 fun save_state _ = raise Fail "Cannot save state -- undefined operation"; |
30 |
32 |
31 end; |
33 end; |