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