Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

--- 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));