src/Pure/PIDE/execution.ML
changeset 56333 38f1422ef473
parent 56305 06dcec23fb8d
child 59348 8a6788917b32
     1.1 --- a/src/Pure/PIDE/execution.ML	Sun Mar 30 21:24:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Mon Mar 31 10:28:08 2014 +0200
     1.3 @@ -122,9 +122,9 @@
     1.4                    Exn.Exn exn =>
     1.5                     (status task [Markup.failed];
     1.6                      status task [Markup.finished];
     1.7 -                    Output.report (Markup.markup_only Markup.bad);
     1.8 +                    Output.report [Markup.markup_only Markup.bad];
     1.9                      if exec_id = 0 then ()
    1.10 -                    else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
    1.11 +                    else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
    1.12                  | Exn.Res _ =>
    1.13                      status task [Markup.finished])
    1.14              in Exn.release result end);