tuned;
authorwenzelm
Wed Apr 11 14:20:51 2012 +0200 (2012-04-11)
changeset 4742457ff63a52c53
parent 47423 8a179a0493e3
child 47425 45e570742e73
tuned;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 11 13:49:09 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 11 14:20:51 2012 +0200
     1.3 @@ -403,10 +403,9 @@
     1.4            (case opt_exec of
     1.5              NONE => true
     1.6            | SOME (exec_id, exec) =>
     1.7 -              not (stable_command exec) orelse
     1.8                (case lookup_entry node0 id of
     1.9                  NONE => true
    1.10 -              | SOME (exec_id0, _) => exec_id <> exec_id0));
    1.11 +              | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec));
    1.12          in SOME (found', (prev, update_flags prev flags)) end;
    1.13      val (found, (common, flags)) =
    1.14        iterate_entries get_common node (false, (NONE, (true, true)));