src/Pure/PIDE/command.ML

     ({command_name: string} -> print_fn option) -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
-  val exec: Exec.context -> exec -> unit
+  val exec: Execution.context -> exec -> unit
 end;
 
 structure Command: COMMAND =
 struct
 

   | Expr _ =>
       Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
         (fn Result res => SOME (res, Result res)
           | expr as Expr (exec_id, e) =>
               uninterruptible (fn restore_attributes => fn () =>
-                if Exec.running context exec_id then
+                if Execution.running context exec_id then
                   let
                     val res = Exn.capture (restore_attributes e) ();
-                    val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
+                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
                   in SOME (res, Result res) end
                 else SOME (Exn.interrupt_exn, expr)) ())
       |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
   |> Exn.release |> ignore;
 

 
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
 val eval_result_state = #state o eval_result;
 
 fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
-  exec_id = exec_id' andalso Exec.is_stable exec_id;
+  exec_id = exec_id' andalso Execution.is_stable exec_id;
 
 local
 
 fun run int tr st =
   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then

 fun print_error tr e =
   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
     List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
 
 fun print_persistent (Print {persistent, ...}) = persistent;
-fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
+fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
 
 in
 
 fun print command_visible command_name eval old_prints =