src/Pure/PIDE/document.ML

              (Toplevel.status tr Markup.finished;
               proof_status tr st';
               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;