# HG changeset patch # User wenzelm # Date 1300734903 -3600 # Node ID 264f8d0e899ff73281071d6b1cad52c9bafa018c # Parent f90040058a24edc07c18adee41f8603125f69dd4 tuned; diff -r f90040058a24 -r 264f8d0e899f src/Pure/General/timing.ML --- 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 (); diff -r f90040058a24 -r 264f8d0e899f src/Pure/Isar/proof.ML --- 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