equal
deleted
inserted
replaced
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) |