tuned;

--- a/src/Pure/PIDE/document.ML	Thu Jul 11 15:56:12 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 16:01:48 2013 +0200
@@ -110,7 +110,7 @@
 
 fun changed_result node node' =
   (case (get_result node, get_result node') of
-    (SOME eval, SOME eval') => #exec_id eval <> #exec_id eval'
+    (SOME eval, SOME eval') => not (Command.eval_same (eval, eval'))
   | (NONE, NONE) => false
   | _ => true);