discontinued notion of "stable" result -- running execution is never canceled;

--- a/src/Pure/PIDE/command.ML	Mon Jul 29 13:00:36 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Jul 29 13:24:15 2013 +0200
@@ -10,7 +10,6 @@
   type eval
   val eval_eq: eval * eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  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
@@ -28,7 +27,7 @@
 structure Command: COMMAND =
 struct
 
-(** memo results -- including physical interrupts! **)
+(** memo results -- including physical interrupts **)
 
 datatype 'a expr =
   Expr of Document_ID.exec * (unit -> 'a) |
@@ -45,11 +44,6 @@
     Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
   | Result res => Exn.release res);
 
-fun memo_stable (Memo v) =
-  (case Synchronized.value v of
-   Expr _ => true
- | Result res => not (Exn.is_interrupt_exn res));
-
 fun memo_finished (Memo v) =
   (case Synchronized.value v of
    Expr _ => false
@@ -125,9 +119,6 @@
 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
 val eval_result_state = #state o eval_result;
 
-fun eval_stable (Eval {exec_id, eval_process}) =
-  Goal.stable_futures exec_id andalso memo_stable eval_process;
-
 local
 
 fun run int tr st =
@@ -220,11 +211,7 @@
 
 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_finished (Print {exec_id, print_process, ...}) =
-  Goal.stable_futures exec_id andalso memo_finished print_process;
+fun print_finished (Print {exec_id, print_process, ...}) = memo_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
@@ -264,8 +251,8 @@
       if command_visible then
         rev (Synchronized.value print_functions) |> map_filter (fn pr =>
           (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
-            SOME print => if print_stable print then SOME print else new_print pr
-          | NONE => new_print pr))
+            NONE => new_print pr
+          | some => some))
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in
     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints

--- a/src/Pure/PIDE/document.ML	Mon Jul 29 13:00:36 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Jul 29 13:24:15 2013 +0200
@@ -41,7 +41,7 @@
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
   perspective: perspective,  (*visible commands, last visible command*)
-  entries: Command.exec option Entries.T * bool,  (*command entries with excecutions, stable*)
+  entries: Command.exec option Entries.T,  (*command entries with excecutions*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
@@ -58,9 +58,8 @@
 val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
 val no_perspective = make_perspective [];
 
-val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
-val clear_node =
-  map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE));
+val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
+val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
 
 
 (* basic components *)
@@ -87,17 +86,11 @@
 val visible_node = is_some o visible_last
 
 fun map_entries f =
-  map_node (fn (header, perspective, (entries, stable), result) =>
-    (header, perspective, (f entries, stable), result));
-fun get_entries (Node {entries = (entries, _), ...}) = entries;
-
-fun entries_stable stable =
-  map_node (fn (header, perspective, (entries, _), result) =>
-    (header, perspective, (entries, stable), result));
-fun stable_entries (Node {entries = (_, stable), ...}) = stable;
+  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
+fun get_entries (Node {entries, ...}) = entries;
 
 fun iterate_entries f = Entries.iterate NONE f o get_entries;
-fun iterate_entries_after start f (Node {entries = (entries, _), ...}) =
+fun iterate_entries_after start f (Node {entries, ...}) =
   (case Entries.get_after entries start of
     NONE => I
   | SOME id => Entries.iterate (SOME id) f entries);
@@ -328,7 +321,6 @@
 type assign_update = Command.exec option Inttab.table;  (*command id -> exec*)
 
 val assign_update_empty: assign_update = Inttab.empty;
-fun assign_update_null (tab: assign_update) = Inttab.is_empty tab;
 fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id;
 fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node;
 
@@ -402,8 +394,7 @@
           val flags' = update_flags prev flags;
           val same' =
             (case (lookup_entry node0 command_id, opt_exec) of
-              (SOME (eval0, _), SOME (eval, _)) =>
-                Command.eval_eq (eval0, eval) andalso Command.eval_stable eval
+              (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval)
             | _ => false);
           val assign_update' = assign_update |> same' ?
             (case opt_exec of
@@ -471,7 +462,7 @@
                 val node_required = is_required name;
               in
                 if imports_changed orelse AList.defined (op =) edits name orelse
-                  not (stable_entries node) orelse not (finished_theory node)
+                  not (finished_theory node)
                 then
                   let
                     val node0 = node_of old_version name;
@@ -512,7 +503,6 @@
 
                     val node' = node
                       |> assign_update_apply assigned_execs
-                      |> entries_stable (assign_update_null updated_execs)
                       |> set_result result;
                     val assigned_node = SOME (name, node');
                     val result_changed = changed_result node0 node';

--- a/src/Pure/goal.ML	Mon Jul 29 13:00:36 2013 +0200
+++ b/src/Pure/goal.ML	Mon Jul 29 13:24:15 2013 +0200
@@ -27,7 +27,6 @@
   val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
   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,9 +180,6 @@
 fun peek_futures id =
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
 
-fun stable_futures id =
-  not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id)));
-
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (_, groups, _) =>
     (Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));