src/Pure/goal.ML
changeset 49830 28d207ba9340
parent 49829 2bc5924b117f
child 49845 9b19c0e81166
equal deleted inserted replaced
49829:2bc5924b117f 49830:28d207ba9340
   158               val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
   158               val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
   159               val _ =
   159               val _ =
   160                 (case result of
   160                 (case result of
   161                   Exn.Res _ => ()
   161                   Exn.Res _ => ()
   162                 | Exn.Exn exn =>
   162                 | Exn.Exn exn =>
   163                     if Exn.is_interrupt exn then ()
   163                     if id = 0 orelse Exn.is_interrupt exn then ()
   164                     else
   164                     else
   165                       (status task [Isabelle_Markup.failed];
   165                       (status task [Isabelle_Markup.failed];
   166                        Output.report (Markup.markup_only Isabelle_Markup.bad);
   166                        Output.report (Markup.markup_only Isabelle_Markup.bad);
   167                        Output.error_msg (ML_Compiler.exn_message exn)));
   167                        Output.error_msg (ML_Compiler.exn_message exn)));
   168               val _ = count_forked ~1;
   168               val _ = count_forked ~1;