# HG changeset patch
# User wenzelm
# Date 1350043530 -7200
# Node ID 2af09163cba18ed8a8b7acdb1b53046b39d8e7f2
# Parent  b28dbb7a45d90d3fd36c25deb05daa9e215f38b5# Parent  28d207ba9340b71aab1ad2ceee2ad5713775b644
merged

diff -r b28dbb7a45d9 -r 2af09163cba1 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Oct 12 12:21:01 2012 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Oct 12 14:05:30 2012 +0200
@@ -113,10 +113,8 @@
       let
         val pos = position_of loc;
         val txt =
-          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
-            ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
-          Position.reported_text pos Isabelle_Markup.report "";
+          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
+          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
       in if hard then err txt else warn txt end;
 
 
diff -r b28dbb7a45d9 -r 2af09163cba1 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Oct 12 12:21:01 2012 +0200
+++ b/src/Pure/goal.ML	Fri Oct 12 14:05:30 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 id = 0 orelse 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];