added profiler interface, keep 'profiling' of PolyML structure;
removed PolyML.Compiler.printInAlphabeticalOrder := false;

--- a/src/Pure/ML-Systems/polyml.ML	Fri Jul 01 14:42:02 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Fri Jul 01 14:42:03 2005 +0200
@@ -8,9 +8,6 @@
 
 (** ML system and platform related **)
 
-PolyML.Compiler.printInAlphabeticalOrder := false;
-
-
 (* cygwin *)
 
 val cygwin_platform =
@@ -148,6 +145,10 @@
 
 (** OS related **)
 
+unless_cygwin
+  use "ML-Systems/polyml-posix.ML";
+
+
 (* system command execution *)
 
 (*execute Unix command which doesn't take any input from stdin and
@@ -177,14 +178,19 @@
   | SOME txt => txt);
 
 
-(* profiling: version that works even with
-ML{*profiling 1*}
-apply \\<dots>
-ML{*profiling 0*}
-*)
+(* profile execution *)
+
+local
+
+fun no_profile () =
+  RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
 
-val profiling: int->unit =
-     RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
+in
 
-unless_cygwin
-  use "ML-Systems/polyml-posix.ML";
+fun profile 0 f x = f x
+  | profile n f x =
+     (RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+      let val y = f x handle exn => (no_profile (); raise exn)
+      in no_profile (); y end);
+
+end;