src/Pure/PIDE/execution.ML
changeset 56303 4cc3f4db3447
parent 56297 3925634718fb
child 56304 40274e4f5ebf
     1.1 --- a/src/Pure/PIDE/execution.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4                      status task [Markup.finished];
     1.5                      Output.report (Markup.markup_only Markup.bad);
     1.6                      if exec_id = 0 then ()
     1.7 -                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
     1.8 +                    else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
     1.9                  | Exn.Res _ =>
    1.10                      status task [Markup.finished])
    1.11              in Exn.release result end);