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)));