# HG changeset patch
# User wenzelm
# Date 1284153118 -7200
# Node ID 85728a4b56205b2756695b368fbb5f3dd0ccde8f
# Parent  3aefd3342978de4f57701a293d148d2532b537e1
avoid extra wrapping for interrupts;

diff -r 3aefd3342978 -r 85728a4b5620 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Sep 09 21:44:52 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 10 23:11:58 2010 +0200
@@ -34,7 +34,7 @@
 exception CONTEXT of Proof.context * exn;
 
 fun exn_context NONE exn = exn
-  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
+  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
 
 (* exn_message *)
diff -r 3aefd3342978 -r 85728a4b5620 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Sep 09 21:44:52 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Sep 10 23:11:58 2010 +0200
@@ -619,7 +619,8 @@
 fun command tr st =
   (case transition (! interact) tr st of
     SOME (st', NONE) => st'
-  | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+  | SOME (_, SOME (exn, info)) =>
+      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
   | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
 fun command_result tr st =