diff options
| -rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 12 | ||||
| -rw-r--r-- | toplevel/stm.ml | 35 | ||||
| -rw-r--r-- | toplevel/vernac_classifier.ml | 4 |
4 files changed, 38 insertions, 14 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 97b038f5c7..28c8c6c9f3 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -424,6 +424,7 @@ type vernac_type = | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type | VtProofStep + | VtProofMode of string | VtQuery of vernac_part_of_script | VtStm of vernac_control * vernac_part_of_script | VtUnknown diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index f79f717124..a4f8641ddb 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -165,15 +165,11 @@ let _ = end } -(* Two new vernacular commands *) -let classify_decl _ = VtProofStep, VtNow - -VERNAC COMMAND EXTEND DeclProof CLASSIFIED BY classify_decl - [ "proof" ] -> [ vernac_decl_proof () ] +VERNAC COMMAND EXTEND DeclProof +[ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END -VERNAC COMMAND EXTEND DeclReturn CLASSIFIED BY classify_decl - - [ "return" ] -> [ vernac_return () ] +VERNAC COMMAND EXTEND DeclReturn +[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] END let none_is_empty = function diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 4a1ce901ca..610e14e8f9 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -354,18 +354,22 @@ end = struct (* {{{ *) let proof_nesting () = Vcs_aux.proof_nesting !vcs let checkout_shallowest_proof_branch () = - if List.mem edit_branch (Vcs_.branches !vcs) then - checkout edit_branch - else + if List.mem edit_branch (Vcs_.branches !vcs) then begin + checkout edit_branch; + match get_branch edit_branch with + | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode + | _ -> assert false + end else let pl = proof_nesting () in try let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in checkout branch; + prerr_endline ("mode:" ^ mode); Proof_global.activate_proof_mode mode with Failure _ -> checkout Branch.master; - Proof_global.disactivate_proof_mode "Classic" (* XXX *) + Proof_global.disactivate_proof_mode "Classic" (* copies the transaction on every open branch *) let propagate_sideff t = @@ -443,7 +447,7 @@ end = struct (* {{{ *) try while true do get_last_job () () done with e -> () (* No failure *) - let command job = + let command job = (* job () *) set_last_job job; if Option.is_empty !worker then worker := Some (Thread.create run_command ()) @@ -1274,6 +1278,27 @@ let process_transaction ~tty verbose c (loc, expr) = VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode mode; Backtrack.record (); if w == VtNow then finish (); `Ok + | VtProofMode _, VtLater -> + anomaly(str"VtProofMode must be executed VtNow") + | VtProofMode mode, VtNow -> + let id = VCS.new_node () in + VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd (x,[])); + VCS.propagate_sideff (Some x); + List.iter + (fun bn -> match VCS.get_branch bn with + | { VCS.root; kind = `Master; pos } -> () + | { VCS.root; kind = `Proof(_,d); pos } -> + VCS.delete_branch bn; + VCS.branch ~root ~pos bn (`Proof(mode,d)) + | { VCS.root; kind = `Edit(_,f,q); pos } -> + VCS.delete_branch bn; + VCS.branch ~root ~pos bn (`Edit(mode,f,q))) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); + finish (); + `Ok | VtProofStep, w -> let id = VCS.new_node () in VCS.commit id (Cmd (x,[])); diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 099f089c3c..f773856ffc 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -19,6 +19,7 @@ let string_of_vernac_type = function | VtQed VtKeep -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" | VtProofStep -> "ProofStep" + | VtProofMode s -> "ProofMode " ^ s | VtQuery b -> "Query" ^ string_of_in_script b | VtStm ((VtFinish|VtJoinDocument|VtObserve _), b) -> "Stm" ^ string_of_in_script b @@ -65,7 +66,8 @@ let rec classify_vernac e = | VernacTime e -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with - | (VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _), _ as x -> x + | ( VtQuery _ | VtProofStep _ | VtSideff _ + | VtStm _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep, VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) |