1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 12 11:28:03 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 12:04:16 2013 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  sig
     1.5    val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     1.6    type eval
     1.7 +  val eval_eq: eval * eval -> bool
     1.8    val eval_result_state: eval -> Toplevel.state
     1.9 -  val eval_same: eval * eval -> bool
    1.10 +  val eval_stable: eval -> bool
    1.11    val eval: (unit -> theory) -> Token.T list -> eval -> eval
    1.12    type print
    1.13    val print: bool -> string -> eval -> print list -> print list option
    1.14 @@ -40,10 +41,15 @@
    1.15  
    1.16  fun memo_result (Memo v) =
    1.17    (case Synchronized.value v of
    1.18 -    Result res => Exn.release res
    1.19 -  | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
    1.20 +    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    1.21 +  | Result res => Exn.release res);
    1.22  
    1.23 -fun memo_exec context (Memo v) =
    1.24 +fun memo_stable (Memo v) =
    1.25 +  (case Synchronized.value v of
    1.26 +   Expr _ => true
    1.27 + | Result res => not (Exn.is_interrupt_exn res));
    1.28 +
    1.29 +fun memo_exec execution_id (Memo v) =
    1.30    (case Synchronized.value v of
    1.31      Result res => res
    1.32    | Expr _ =>
    1.33 @@ -51,23 +57,24 @@
    1.34          (fn Result res => SOME (res, Result res)
    1.35            | expr as Expr (exec_id, e) =>
    1.36                uninterruptible (fn restore_attributes => fn () =>
    1.37 -                if Execution.running context exec_id then
    1.38 +                if Execution.running execution_id exec_id then
    1.39                    let
    1.40                      val res = Exn.capture (restore_attributes e) ();
    1.41 -                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
    1.42 +                    val _ = Execution.finished exec_id;
    1.43                    in SOME (res, Result res) end
    1.44                  else SOME (Exn.interrupt_exn, expr)) ())
    1.45        |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.46    |> Exn.release |> ignore;
    1.47  
    1.48 -fun memo_fork params context (Memo v) =
    1.49 +fun memo_fork params execution_id (Memo v) =
    1.50    (case Synchronized.value v of
    1.51      Result _ => ()
    1.52 -  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec context (Memo v))));
    1.53 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
    1.54  
    1.55  end;
    1.56  
    1.57  
    1.58 +
    1.59  (** main phases of execution **)
    1.60  
    1.61  (* read *)
    1.62 @@ -109,11 +116,13 @@
    1.63  
    1.64  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    1.65  
    1.66 +fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.67 +
    1.68  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.69  val eval_result_state = #state o eval_result;
    1.70  
    1.71 -fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
    1.72 -  exec_id = exec_id' andalso Execution.is_stable exec_id;
    1.73 +fun eval_stable (Eval {exec_id, eval_process}) =
    1.74 +  Goal.stable_futures exec_id andalso memo_stable eval_process;
    1.75  
    1.76  local
    1.77  
    1.78 @@ -197,9 +206,12 @@
    1.79    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn =>
    1.80      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.81  
    1.82 +fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.83 +
    1.84 +fun print_stable (Print {exec_id, print_process, ...}) =
    1.85 +  Goal.stable_futures exec_id andalso memo_stable print_process;
    1.86 +
    1.87  fun print_persistent (Print {persistent, ...}) = persistent;
    1.88 -fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
    1.89 -fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.90  
    1.91  in
    1.92  
    1.93 @@ -276,15 +288,15 @@
    1.94  
    1.95  local
    1.96  
    1.97 -fun run_print context (Print {name, pri, print_process, ...}) =
    1.98 +fun run_print execution_id (Print {name, pri, print_process, ...}) =
    1.99    (if Multithreading.enabled () then
   1.100      memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
   1.101 -  else memo_exec) context print_process;
   1.102 +  else memo_exec) execution_id print_process;
   1.103  
   1.104  in
   1.105  
   1.106 -fun exec context (Eval {eval_process, ...}, prints) =
   1.107 -  (memo_exec context eval_process; List.app (run_print context) prints);
   1.108 +fun exec execution_id (Eval {eval_process, ...}, prints) =
   1.109 +  (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
   1.110  
   1.111  end;
   1.112