pure Timing.timing, without any exception handling;
authorwenzelm
Sun Mar 20 21:44:38 2011 +0100 (2011-03-20 ago)
changeset 420131694cc477045
parent 42012 2c3fe3cbebae
child 42014 75417ef605ba
pure Timing.timing, without any exception handling;
clarified cond_timeit: propagate interrupt without side-effect;
src/Pure/General/timing.ML
     1.1 --- a/src/Pure/General/timing.ML	Sun Mar 20 21:28:11 2011 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Sun Mar 20 21:44:38 2011 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    type start
     1.5    val start: unit -> start
     1.6    val result: start -> timing
     1.7 +  val timing: ('a -> 'b) -> 'a -> timing * 'b
     1.8    val message: timing -> string
     1.9  end
    1.10  
    1.11 @@ -57,6 +58,12 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +fun timing f x =
    1.16 +  let
    1.17 +    val start = start ();
    1.18 +    val y = f x;
    1.19 +  in (result start, y) end;
    1.20 +
    1.21  
    1.22  (* timing messages *)
    1.23  
    1.24 @@ -68,11 +75,12 @@
    1.25  fun cond_timeit enabled msg e =
    1.26    if enabled then
    1.27      let
    1.28 -      val timing_start = start ();
    1.29 -      val res = Exn.capture e ();
    1.30 -      val end_msg = message (result timing_start);
    1.31 -      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    1.32 -    in Exn.release res end
    1.33 +      val (timing, result) = timing (Exn.capture e) ();
    1.34 +      val end_msg = message timing;
    1.35 +      val _ =
    1.36 +        if Exn.is_interrupt_exn result then ()
    1.37 +        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    1.38 +    in Exn.release result end
    1.39    else e ();
    1.40  
    1.41  fun timeit e = cond_timeit true "" e;