equal
deleted
inserted
replaced
5 |
5 |
6 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x). |
6 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x). |
7 *) |
7 *) |
8 |
8 |
9 (** ML system and platform related **) |
9 (** ML system and platform related **) |
10 |
|
11 PolyML.Compiler.printInAlphabeticalOrder := false; |
|
12 |
|
13 |
10 |
14 (* cygwin *) |
11 (* cygwin *) |
15 |
12 |
16 val cygwin_platform = |
13 val cygwin_platform = |
17 let val n = size ml_platform |
14 let val n = size ml_platform |
146 |
143 |
147 |
144 |
148 |
145 |
149 (** OS related **) |
146 (** OS related **) |
150 |
147 |
|
148 unless_cygwin |
|
149 use "ML-Systems/polyml-posix.ML"; |
|
150 |
|
151 |
151 (* system command execution *) |
152 (* system command execution *) |
152 |
153 |
153 (*execute Unix command which doesn't take any input from stdin and |
154 (*execute Unix command which doesn't take any input from stdin and |
154 sends its output to stdout; could be done more easily by Unix.execute, |
155 sends its output to stdout; could be done more easily by Unix.execute, |
155 but that function doesn't use the PATH*) |
156 but that function doesn't use the PATH*) |
175 (case OS.Process.getEnv var of |
176 (case OS.Process.getEnv var of |
176 NONE => "" |
177 NONE => "" |
177 | SOME txt => txt); |
178 | SOME txt => txt); |
178 |
179 |
179 |
180 |
180 (* profiling: version that works even with |
181 (* profile execution *) |
181 ML{*profiling 1*} |
|
182 apply \\<dots> |
|
183 ML{*profiling 0*} |
|
184 *) |
|
185 |
182 |
186 val profiling: int->unit = |
183 local |
187 RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler; |
|
188 |
184 |
189 unless_cygwin |
185 fun no_profile () = |
190 use "ML-Systems/polyml-posix.ML"; |
186 RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
|
187 |
|
188 in |
|
189 |
|
190 fun profile 0 f x = f x |
|
191 | profile n f x = |
|
192 (RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
|
193 let val y = f x handle exn => (no_profile (); raise exn) |
|
194 in no_profile (); y end); |
|
195 |
|
196 end; |