no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
authorwenzelm
Fri, 12 Oct 2012 13:55:13 +0200
changeset 49830 28d207ba9340
parent 49829 2bc5924b117f
child 49832 2af09163cba1
no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Oct 12 13:46:41 2012 +0200
+++ b/src/Pure/goal.ML	Fri Oct 12 13:55:13 2012 +0200
@@ -160,7 +160,7 @@
                 (case result of
                   Exn.Res _ => ()
                 | Exn.Exn exn =>
-                    if Exn.is_interrupt exn then ()
+                    if id = 0 orelse Exn.is_interrupt exn then ()
                     else
                       (status task [Isabelle_Markup.failed];
                        Output.report (Markup.markup_only Isabelle_Markup.bad);