# HG changeset patch
# User wenzelm
# Date 1373551308 -7200
# Node ID d7871f38ffb4490b6c9137ff8fb5bf5b8b663cdb
# Parent  cad097fb46deceae4c5bf7cab60721f2419f9e1b
tuned;

diff -r cad097fb46de -r d7871f38ffb4 src/Pure/PIDE/document.ML
--- 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);