src/Pure/PIDE/document.ML

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