equal
deleted
inserted
replaced
36 |
36 |
37 if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else (); |
37 if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else (); |
38 |
38 |
39 structure ML_System = |
39 structure ML_System = |
40 struct |
40 struct |
41 |
41 open ML_System; |
42 open ML_System; |
42 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
43 |
43 val save_state = PolyML.SaveState.saveState o ml_platform_path; |
44 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
45 val save_state = PolyML.SaveState.saveState; |
|
46 |
|
47 end; |
44 end; |
48 |
45 |
49 |
46 |
50 (* exceptions *) |
47 (* exceptions *) |
51 |
48 |