src/Pure/PIDE/document.ML
changeset 47424 57ff63a52c53
parent 47420 0dbe6c69eda2
child 47628 3275758d274e
equal deleted inserted replaced
47423:8a179a0493e3 47424:57ff63a52c53
   401       else
   401       else
   402         let val found' =
   402         let val found' =
   403           (case opt_exec of
   403           (case opt_exec of
   404             NONE => true
   404             NONE => true
   405           | SOME (exec_id, exec) =>
   405           | SOME (exec_id, exec) =>
   406               not (stable_command exec) orelse
       
   407               (case lookup_entry node0 id of
   406               (case lookup_entry node0 id of
   408                 NONE => true
   407                 NONE => true
   409               | SOME (exec_id0, _) => exec_id <> exec_id0));
   408               | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec));
   410         in SOME (found', (prev, update_flags prev flags)) end;
   409         in SOME (found', (prev, update_flags prev flags)) end;
   411     val (found, (common, flags)) =
   410     val (found, (common, flags)) =
   412       iterate_entries get_common node (false, (NONE, (true, true)));
   411       iterate_entries get_common node (false, (NONE, (true, true)));
   413   in
   412   in
   414     if found then (common, flags)
   413     if found then (common, flags)