--- a/src/Pure/Isar/runtime.ML Thu Sep 09 18:18:34 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Thu Sep 09 18:21:06 2010 +0200
@@ -110,9 +110,14 @@
|> debugging
|> Future.interruptible_task;
-fun toplevel_error output_exn f x =
- let val ctxt = Option.map Context.proof_of (Context.thread_data ())
- in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
+fun toplevel_error output_exn f x = f x
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val ctxt = Option.map Context.proof_of (Context.thread_data ());
+ val _ = output_exn (exn_context ctxt exn);
+ in raise TOPLEVEL_ERROR end;
end;