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