# 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 =