1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 23:24:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 11:07:02 2013 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    type exec = eval * print list
     1.5    val no_exec: exec
     1.6    val exec_ids: exec option -> Document_ID.exec list
     1.7 -  val exec: Exec.context -> exec -> unit
     1.8 +  val exec: Execution.context -> exec -> unit
     1.9  end;
    1.10  
    1.11  structure Command: COMMAND =
    1.12 @@ -51,10 +51,10 @@
    1.13          (fn Result res => SOME (res, Result res)
    1.14            | expr as Expr (exec_id, e) =>
    1.15                uninterruptible (fn restore_attributes => fn () =>
    1.16 -                if Exec.running context exec_id then
    1.17 +                if Execution.running context exec_id then
    1.18                    let
    1.19                      val res = Exn.capture (restore_attributes e) ();
    1.20 -                    val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.21 +                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
    1.22                    in SOME (res, Result res) end
    1.23                  else SOME (Exn.interrupt_exn, expr)) ())
    1.24        |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.25 @@ -113,7 +113,7 @@
    1.26  val eval_result_state = #state o eval_result;
    1.27  
    1.28  fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
    1.29 -  exec_id = exec_id' andalso Exec.is_stable exec_id;
    1.30 +  exec_id = exec_id' andalso Execution.is_stable exec_id;
    1.31  
    1.32  local
    1.33  
    1.34 @@ -198,7 +198,7 @@
    1.35      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.36  
    1.37  fun print_persistent (Print {persistent, ...}) = persistent;
    1.38 -fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
    1.39 +fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
    1.40  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.41  
    1.42  in