--- a/src/Pure/General/timing.ML Mon Mar 21 17:14:52 2011 +0100
+++ b/src/Pure/General/timing.ML Mon Mar 21 20:15:03 2011 +0100
@@ -75,11 +75,9 @@
fun cond_timeit enabled msg e =
if enabled then
let
- val (timing, result) = timing (Exn.capture e) ();
+ val (timing, result) = timing (Exn.interruptible_capture e) ();
val end_msg = message timing;
- val _ =
- if Exn.is_interrupt_exn result then ()
- else warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
+ val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
in Exn.release result end
else e ();
--- a/src/Pure/Isar/proof.ML Mon Mar 21 17:14:52 2011 +0100
+++ b/src/Pure/Isar/proof.ML Mon Mar 21 20:15:03 2011 +0100
@@ -999,7 +999,7 @@
val test_proof =
try (local_skip_proof true)
|> Unsynchronized.setmp testing true
- |> Exn.capture;
+ |> Exn.interruptible_capture;
fun after_qed' results =
refine_goals print_rule (context_of state) (flat results)
@@ -1012,9 +1012,7 @@
(case test_proof goal_state of
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
- | Exn.Exn exn =>
- if Exn.is_interrupt exn then reraise exn
- else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+ | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
in