src/Pure/PIDE/command.ML

--- a/src/Pure/PIDE/command.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -196,7 +196,7 @@
         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
-            else ML_Compiler.exn_messages_ids exn)) ();
+            else Runtime.exn_messages_ids exn)) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
@@ -276,10 +276,10 @@
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr opt_context e =
-  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
+  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
-      else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+      else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
 
@@ -319,7 +319,7 @@
       let
         val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
       in
-        (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
+        (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))