# HG changeset patch
# User wenzelm
# Date 1275317148 -7200
# Node ID e8b1c3a0562c4deb41c1b6802396402ec3134c1f
# Parent  c40c9b05952c0e276da2bb4a2486046ce79b86ec
Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

diff -r c40c9b05952c -r e8b1c3a0562c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon May 31 10:29:04 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 31 16:45:48 2010 +0200
@@ -643,6 +643,7 @@
     Exn.Result () =>
       (case transition true tr st of
         SOME (st', NONE) => (status tr Markup.finished; SOME st')
+      | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
       | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
       | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));