equal
deleted
inserted
replaced
68 val implode = SML90.implode; |
68 val implode = SML90.implode; |
69 |
69 |
70 fun quit () = exit 0; |
70 fun quit () = exit 0; |
71 |
71 |
72 |
72 |
73 (* ML system identification *) |
73 (* ML system operations *) |
74 |
74 |
75 use "ML-Systems/ml_system.ML"; |
75 use "ML-Systems/ml_system.ML"; |
|
76 |
|
77 structure ML_System = |
|
78 struct |
|
79 |
|
80 open ML_System; |
|
81 |
|
82 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
83 val save_state = PolyML.SaveState.saveState; |
|
84 |
|
85 end; |
76 |
86 |
77 |
87 |
78 (* ML runtime system *) |
88 (* ML runtime system *) |
79 |
89 |
80 val exception_trace = PolyML.exception_trace; |
90 val exception_trace = PolyML.exception_trace; |
88 val res = Exn.capture f x; |
98 val res = Exn.capture f x; |
89 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
99 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
90 in Exn.release res end; |
100 in Exn.release res end; |
91 |
101 |
92 val pointer_eq = PolyML.pointerEq; |
102 val pointer_eq = PolyML.pointerEq; |
93 |
|
94 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
95 |
103 |
96 |
104 |
97 (* ML compiler *) |
105 (* ML compiler *) |
98 |
106 |
99 structure ML_Name_Space = |
107 structure ML_Name_Space = |