# HG changeset patch
# User wenzelm
# Date 1350042401 -7200
# Node ID 2bc5924b117facbae7e821621c9f2d09ef544733
# Parent  5631ee09929396b1dae2ab7af095616df1f7aa4b
do not treat interrupt as error here, to avoid confusion in log etc.;

diff -r 5631ee099293 -r 2bc5924b117f src/Pure/goal.ML
--- 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];