From 58270be4668ab87e5f2d0d06c820bd457ae1aa01 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 11 Jul 2014 10:34:55 +0200
Subject: STM: flag to turn off branch reopening

This is useful if a UI does not support that
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 8b44e3dbf8..659cfe3c8d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1232,7 +1232,7 @@ let collect_proof cur hd brkind id =
      if is_defined cur then `Sync (no_name,`Transparent)
      else
        let rc = collect (Some cur) [] id in
-       if not (State.is_cached id) then rc
+       if not (State.is_cached id) || !Flags.async_proofs_always_delegate then rc
        else (* we already have the proof, no gain in delaying *)
          match rc with
          | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated)
@@ -1920,7 +1920,7 @@ let edit_at id =
       | _, Some _, None -> assert false
       | false, Some qed_id, Some mode ->
           let tip = VCS.cur_tip () in
-          if has_failed qed_id then reopen_branch id mode qed_id tip
+          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch then reopen_branch id mode qed_id tip
           else backto id
       | true, Some qed_id, Some mode ->
           if on_cur_branch id then begin
-- 
cgit v1.2.3