diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 46 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 1 |
2 files changed, 27 insertions, 20 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ad94b68077..e970a02eed 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2734,7 +2734,6 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - if e = CErrors.Drop then Exninfo.iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2803,6 +2802,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Meta *) | VtMeta, _ -> let id, w = Backtrack.undo_vernac_classifier expr in + (* Special case Backtrack, as it is never part of a script. See #6240 *) + let part_of_script = begin match Vernacprop.under_control expr with + | VernacBacktrack _ -> false + | _ -> part_of_script + end in process_back_meta_command ~part_of_script ~newtip ~head id x w (* Query *) | VtQuery (false,route), VtNow -> @@ -2880,23 +2884,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - (* Side effect on all branches *) - | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); - `Ok - + (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; - VCS.commit id (mkTransCmd x l in_proof `MainQueue); - (* We can't replay a Definition since universes may be differently - * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with - | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv - | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); + | `Proof _ -> + VCS.checkout VCS.Branch.master; + VCS.commit id (mkTransCmd x l true `MainQueue); + (* We can't replay a Definition since universes may be differently + * inferred. This holds in Coq >= 8.5 *) + let action = match Vernacprop.under_control x.expr with + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; + end; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2925,9 +2928,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; end else begin - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Proof _ -> + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + (* We hope it can be replayed, but we can't really know *) + VCS.propagate_sideff ~action:(ReplayCommand x); + end; VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f68c8b326b..9a8af3a58c 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,7 +185,6 @@ let classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) - | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) |