tuned;
authorwenzelm
Mon Mar 21 20:15:03 2011 +0100 (2011-03-21)
changeset 42042264f8d0e899f
parent 42041 f90040058a24
child 42043 2055515c9d3f
tuned;
src/Pure/General/timing.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/General/timing.ML	Mon Mar 21 17:14:52 2011 +0100
     1.2 +++ b/src/Pure/General/timing.ML	Mon Mar 21 20:15:03 2011 +0100
     1.3 @@ -75,11 +75,9 @@
     1.4  fun cond_timeit enabled msg e =
     1.5    if enabled then
     1.6      let
     1.7 -      val (timing, result) = timing (Exn.capture e) ();
     1.8 +      val (timing, result) = timing (Exn.interruptible_capture e) ();
     1.9        val end_msg = message timing;
    1.10 -      val _ =
    1.11 -        if Exn.is_interrupt_exn result then ()
    1.12 -        else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    1.13 +      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
    1.14      in Exn.release result end
    1.15    else e ();
    1.16  
     2.1 --- a/src/Pure/Isar/proof.ML	Mon Mar 21 17:14:52 2011 +0100
     2.2 +++ b/src/Pure/Isar/proof.ML	Mon Mar 21 20:15:03 2011 +0100
     2.3 @@ -999,7 +999,7 @@
     2.4      val test_proof =
     2.5        try (local_skip_proof true)
     2.6        |> Unsynchronized.setmp testing true
     2.7 -      |> Exn.capture;
     2.8 +      |> Exn.interruptible_capture;
     2.9  
    2.10      fun after_qed' results =
    2.11        refine_goals print_rule (context_of state) (flat results)
    2.12 @@ -1012,9 +1012,7 @@
    2.13        (case test_proof goal_state of
    2.14          Exn.Result (SOME _) => goal_state
    2.15        | Exn.Result NONE => error (fail_msg (context_of goal_state))
    2.16 -      | Exn.Exn exn =>
    2.17 -          if Exn.is_interrupt exn then reraise exn
    2.18 -          else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    2.19 +      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
    2.20    end;
    2.21  
    2.22  in