refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

--- a/src/Pure/Isar/runtime.ML	Thu Sep 09 18:18:34 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Sep 09 18:21:06 2010 +0200
@@ -110,9 +110,14 @@
   |> debugging
   |> Future.interruptible_task;
 
-fun toplevel_error output_exn f x =
-  let val ctxt = Option.map Context.proof_of (Context.thread_data ())
-  in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
+fun toplevel_error output_exn f x = f x
+  handle exn =>
+    if Exn.is_interrupt exn then reraise exn
+    else
+      let
+        val ctxt = Option.map Context.proof_of (Context.thread_data ());
+        val _ = output_exn (exn_context ctxt exn);
+      in raise TOPLEVEL_ERROR end;
 
 end;
 

--- a/src/Pure/PIDE/document.ML	Thu Sep 09 18:18:34 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Sep 09 18:21:06 2010 +0200
@@ -238,7 +238,10 @@
               if int then () else async_state tr st'));
       in result end
   | Exn.Exn exn =>
-     (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+      if Exn.is_interrupt exn then reraise exn
+      else
+       (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
+        Toplevel.status tr Markup.failed; NONE));
 
 end;