src/Pure/ML-Systems/polyml.ML
changeset 24851 4e304aac841a
parent 24688 a5754ca5c510
child 25023 52eb78ebb370
equal deleted inserted replaced
24850:0cfd722ab579 24851:4e304aac841a
   200   | SOME txt => txt);
   200   | SOME txt => txt);
   201 
   201 
   202 
   202 
   203 (* profile execution *)
   203 (* profile execution *)
   204 
   204 
   205 local
       
   206 
       
   207 fun no_profile () =
       
   208   RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
       
   209 
       
   210 in
       
   211 
       
   212 fun profile 0 f x = f x
   205 fun profile 0 f x = f x
   213   | profile n f x =
   206   | profile n f x =
   214      (RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   207       let
   215       let val y = f x handle exn => (no_profile (); raise exn)
   208         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   216       in no_profile (); y end);
   209         val res = Exn.capture f x;
   217 
   210         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   218 end;
   211       in Exn.release res end;
       
   212