# HG changeset patch
# User wenzelm
# Date 1334146851 -7200
# Node ID 57ff63a52c5374de1efad841c80efb3aabd083f7
# Parent  8a179a0493e3e85a90b2493a819ef56188bebc26
tuned;

diff -r 8a179a0493e3 -r 57ff63a52c53 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Apr 11 13:49:09 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 11 14:20:51 2012 +0200
@@ -403,10 +403,9 @@
           (case opt_exec of
             NONE => true
           | SOME (exec_id, exec) =>
-              not (stable_command exec) orelse
               (case lookup_entry node0 id of
                 NONE => true
-              | SOME (exec_id0, _) => exec_id <> exec_id0));
+              | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec));
         in SOME (found', (prev, update_flags prev flags)) end;
     val (found, (common, flags)) =
       iterate_entries get_common node (false, (NONE, (true, true)));