clarified execution: maintain running execs only, check "stable" separately via memo (again);
tuned signatures;

--- a/src/Pure/PIDE/command.ML	Fri Jul 12 11:28:03 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 12 12:04:16 2013 +0200
@@ -8,8 +8,9 @@
 sig
   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
   type eval
+  val eval_eq: eval * eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval_same: eval * eval -> bool
+  val eval_stable: eval -> bool
   val eval: (unit -> theory) -> Token.T list -> eval -> eval
   type print
   val print: bool -> string -> eval -> print list -> print list option
@@ -40,10 +41,15 @@
 
 fun memo_result (Memo v) =
   (case Synchronized.value v of
-    Result res => Exn.release res
-  | Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
+    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
+  | Result res => Exn.release res);
 
-fun memo_exec context (Memo v) =
+fun memo_stable (Memo v) =
+  (case Synchronized.value v of
+   Expr _ => true
+ | Result res => not (Exn.is_interrupt_exn res));
+
+fun memo_exec execution_id (Memo v) =
   (case Synchronized.value v of
     Result res => res
   | Expr _ =>
@@ -51,23 +57,24 @@
         (fn Result res => SOME (res, Result res)
           | expr as Expr (exec_id, e) =>
               uninterruptible (fn restore_attributes => fn () =>
-                if Execution.running context exec_id then
+                if Execution.running execution_id exec_id then
                   let
                     val res = Exn.capture (restore_attributes e) ();
-                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
+                    val _ = Execution.finished exec_id;
                   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 memo_fork params context (Memo v) =
+fun memo_fork params execution_id (Memo v) =
   (case Synchronized.value v of
     Result _ => ()
-  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec context (Memo v))));
+  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
 
 end;
 
 
+
 (** main phases of execution **)
 
 (* read *)
@@ -109,11 +116,13 @@
 
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
 
+fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
+
 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 Execution.is_stable exec_id;
+fun eval_stable (Eval {exec_id, eval_process}) =
+  Goal.stable_futures exec_id andalso memo_stable eval_process;
 
 local
 
@@ -197,9 +206,12 @@
   (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_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
+
+fun print_stable (Print {exec_id, print_process, ...}) =
+  Goal.stable_futures exec_id andalso memo_stable print_process;
+
 fun print_persistent (Print {persistent, ...}) = persistent;
-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
 
@@ -276,15 +288,15 @@
 
 local
 
-fun run_print context (Print {name, pri, print_process, ...}) =
+fun run_print execution_id (Print {name, pri, print_process, ...}) =
   (if Multithreading.enabled () then
     memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
-  else memo_exec) context print_process;
+  else memo_exec) execution_id print_process;
 
 in
 
-fun exec context (Eval {eval_process, ...}, prints) =
-  (memo_exec context eval_process; List.app (run_print context) prints);
+fun exec execution_id (Eval {eval_process, ...}, prints) =
+  (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
 
 end;
 

--- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 12 12:04:16 2013 +0200
@@ -108,7 +108,7 @@
 
 fun changed_result node node' =
   (case (get_result node, get_result node') of
-    (SOME eval, SOME eval') => not (Command.eval_same (eval, eval'))
+    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
   | (NONE, NONE) => false
   | _ => true);
 
@@ -401,7 +401,8 @@
           val flags' = update_flags prev flags;
           val same' =
             (case (lookup_entry node0 command_id, opt_exec) of
-              (SOME (eval0, _), SOME (eval, _)) => Command.eval_same (eval0, eval)
+              (SOME (eval0, _), SOME (eval, _)) =>
+                Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
             | _ => false);
           val assign_update' = assign_update |> same' ?
             (case opt_exec of
@@ -445,7 +446,7 @@
 
 fun cancel_old_execs node0 (command_id, exec_ids) =
   subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
-  |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
+  |> map_filter (Execution.peek #> Option.map (tap Future.cancel_group));
 
 in
 

--- a/src/Pure/PIDE/execution.ML	Fri Jul 12 11:28:03 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 12:04:16 2013 +0200
@@ -11,18 +11,17 @@
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
   val running: Document_ID.execution -> Document_ID.exec -> bool
-  val finished: Document_ID.exec -> bool -> unit
-  val is_stable: Document_ID.exec -> bool
-  val peek_running: Document_ID.exec -> Future.group option
-  val purge_canceled: unit -> unit
-  val terminate_all: unit -> unit
+  val finished: Document_ID.exec -> unit
+  val peek: Document_ID.exec -> Future.group option
+  val snapshot: unit -> Future.group list
 end;
 
 structure Execution: EXECUTION =
 struct
 
-type status = Future.group option;  (*SOME group: running, NONE: canceled*)
-val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
+val state =
+  Synchronized.var "Execution.state"
+    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
 
 
 (* unique running execution *)
@@ -48,46 +47,23 @@
         val continue = execution_id = execution_id';
         val execs' =
           if continue then
-            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
+            Inttab.update_new (exec_id, Future.the_worker_group ()) execs
               handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
           else execs;
       in SOME (continue, (execution_id', execs')) end);
 
-fun finished exec_id stable =
+fun finished exec_id =
   Synchronized.change state
     (apsnd (fn execs =>
-      if not (Inttab.defined execs exec_id) then
-        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
-      else if stable then Inttab.delete exec_id execs
-      else Inttab.update (exec_id, NONE) execs));
-
-fun is_stable exec_id =
-  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
-  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
-    NONE => true
-  | SOME status => is_some status);
-
-fun peek_running exec_id =
-  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
-    SOME (SOME group) => SOME group
-  | _ => NONE);
+      Inttab.delete exec_id execs
+        handle Inttab.UNDEF bad =>
+          error ("Attempt to finish unknown execution: " ^ Document_ID.print bad)));
 
-fun purge_canceled () =
-  Synchronized.guarded_access state
-    (fn (execution_id, execs) =>
-      let
-        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
-        val execs' = fold Inttab.delete canceled execs;
-      in SOME ((), (execution_id, execs')) end);
+fun peek exec_id =
+  Inttab.lookup (snd (Synchronized.value state)) exec_id;
 
-fun terminate_all () =
-  let
-    val groups =
-      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
-        (snd (Synchronized.value state)) [];
-    val _ = List.app Future.cancel_group groups;
-    val _ = List.app Future.terminate groups;
-  in () end;
+fun snapshot () =
+  Inttab.fold (cons o #2) (snd (Synchronized.value state)) [];
 
 end;
 

--- a/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:28:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Jul 12 12:04:16 2013 +0200
@@ -21,7 +21,13 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.cancel_execution"
-    (fn [] => (Execution.discontinue (); Execution.terminate_all ()));
+    (fn [] =>
+      let
+        val _ = Execution.discontinue ();
+        val groups = Execution.snapshot ();
+        val _ = List.app Future.cancel_group groups;
+        val _ = List.app Future.terminate groups;
+      in () end);
 
 val _ =
   Isabelle_Process.protocol_command "Document.update"
@@ -54,7 +60,6 @@
         val (assign_update, state') = Document.update old_id new_id edits state;
 
         val _ = List.app Future.cancel_group (Goal.reset_futures ());
-        val _ = Execution.purge_canceled ();
         val _ = Isabelle_Process.reset_tracing ();
 
         val _ =

--- a/src/Pure/goal.ML	Fri Jul 12 11:28:03 2013 +0200
+++ b/src/Pure/goal.ML	Fri Jul 12 12:04:16 2013 +0200
@@ -27,7 +27,8 @@
   val norm_result: thm -> thm
   val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
-  val peek_futures: serial -> unit future list
+  val peek_futures: int -> unit future list
+  val stable_futures: int-> bool
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
   val skip_proofs_enabled: unit -> bool
@@ -181,6 +182,9 @@
 fun peek_futures id =
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
 
+fun stable_futures id =
+  not (Par_Exn.is_interrupted (Future.join_results (peek_futures id)));
+
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (_, groups, _) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));