diff -r 0d68d108d7e0 -r 33a133d50616 src/Pure/PIDE/document.ML
--- 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