--- a/src/Pure/goal.ML Fri Oct 12 11:03:23 2012 +0200
+++ b/src/Pure/goal.ML Fri Oct 12 13:46:41 2012 +0200
@@ -160,9 +160,11 @@
(case result of
Exn.Res _ => ()
| Exn.Exn exn =>
- (status task [Isabelle_Markup.failed];
- Output.report (Markup.markup_only Isabelle_Markup.bad);
- Output.error_msg (ML_Compiler.exn_message exn)));
+ if Exn.is_interrupt exn then ()
+ else
+ (status task [Isabelle_Markup.failed];
+ Output.report (Markup.markup_only Isabelle_Markup.bad);
+ Output.error_msg (ML_Compiler.exn_message exn)));
val _ = count_forked ~1;
in Exn.release result end);
val _ = status (Future.task_of future) [Isabelle_Markup.forked];