diff options
| author | Enrico Tassi | 2015-11-02 15:01:15 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-11-02 15:19:41 +0100 |
| commit | 559c0a4a40410745f73822e893b3d1581056ea7a (patch) | |
| tree | 84f3847e36a4058ff31814e196b45d2e7e23c6fe | |
| parent | b49c80406f518d273056b2143f55e23deeea2813 (diff) | |
STM: never reopen a branch containing side effects
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 42be4fca71..a6a64f2094 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,6 +2317,12 @@ let edit_at id = | { step = `Fork _ } -> false | { next } -> aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in + let rec is_pure id = + let view = VCS.visit id in + match view.step with + | `Cmd _ -> is_pure view.next + | `Fork _ -> true + | _ -> false in let is_ancestor_of_cur_branch id = Vcs_.NodeSet.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in @@ -2377,7 +2383,7 @@ let edit_at id = | _, Some _, None -> assert false | false, Some (qed_id,start), Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch + if has_failed qed_id && is_pure (VCS.visit qed_id).next && not !Flags.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some (qed_id,_), Some(mode,bn) -> |