src/Pure/PIDE/command.ML

 local
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
     SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE));
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
+  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
 
 fun check_cmts tr cmts st =
   Toplevel.setmp_thread_position tr
     (fn () => cmts
       |> maps (fn cmt =>
         (Thy_Output.check_text (Token.source_position_of cmt) st; [])
-          handle exn => ML_Compiler.exn_messages exn)) ();
+          handle exn => ML_Compiler.exn_messages_ids exn)) ();
 
 fun timing tr t =
   if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
 
 fun proof_status tr st =

       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
       val errs = errs1 @ errs2;
       val _ = timing tr (Timing.result start);
       val _ = Toplevel.status tr Markup.finished;
-      val _ = List.app (Toplevel.error_msg tr) errs;
+      val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
     in
       (case result of
         NONE =>
           let
             val _ = if null errs then Exn.interrupt () else ();