diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 23 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 50 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 2 |
4 files changed, 55 insertions, 26 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 232edda0fd..af6aa4bf59 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -66,7 +66,7 @@ type command_mode = | Mode_none let mode_of_pftreestate pts = - (* spiwack: it was "top_goal_..." but this should be fine *) + (* spiwack: it used to be "top_goal_..." but this should be fine *) let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let goal = List.hd goals in if info.get (Goal.V82.extra sigma goal) = None then @@ -96,10 +96,25 @@ let get_stack pts = let info = get_info sigma (List.hd goals) in info.pm_stack + +let proof_focus = Proof.new_focus_kind () +let proof_cond = Proof.no_cond proof_focus + +let focus p = + let inf = get_stack p in + Proof.focus proof_cond inf 1 p + +let unfocus = Proof.unfocus proof_focus + +let maximal_unfocus = Proof_global.maximal_unfocus proof_focus + let get_top_stack pts = - let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in - let info = get_info sigma gl in - info.pm_stack + try + Proof.get_at_focus proof_focus pts + with Proof.NoSuchFocus -> + let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in + let info = get_info sigma gl in + info.pm_stack let get_last env = try diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 72c46c7e7d..4e636598f9 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -70,3 +70,9 @@ val get_stack : Proof.proof -> stack_info list val get_top_stack : Proof.proof -> stack_info list val get_last: Environ.env -> identifier + +val focus : Proof.proof -> unit + +val unfocus : Proof.proof -> unit + +val maximal_unfocus : Proof.proof -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index cee4d7271d..549b1f1465 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -111,17 +111,15 @@ let assert_postpone id t = (* start a proof *) -let proof_focus = Proof.new_focus_kind () -let proof_cond = Proof.no_cond proof_focus let start_proof_tac gls= let info={pm_stack=[]} in tcl_change_info info gls let go_to_proof_mode () = - Pfedit.by start_proof_tac ; + Pfedit.by start_proof_tac; let p = Proof_global.give_me_the_proof () in - Proof.focus proof_cond 1 p + Decl_mode.focus p (* closing gaps *) @@ -154,12 +152,14 @@ let mark_rule_as_done = function (* post-instruction focus management *) +(* spiwack: This used to fail if there was no focusing command + above, but I don't think it ever happened. I hope it doesn't mess + things up*) let goto_current_focus pts = - Proof.unfocus proof_focus pts + Decl_mode.maximal_unfocus pts let goto_current_focus_or_top pts = - try goto_current_focus pts - with Util.UserError _ -> () + goto_current_focus pts (* return *) @@ -172,6 +172,7 @@ let close_tactic_mode pts = goto_current_focus pts2 let return_from_tactic_mode () = + (* arnaud: la commande return ne fonctionne pas *) Util.anomaly "Todo: Decl_proof_instr.return_from_tactic_mode" (* end proof/claim *) @@ -180,7 +181,12 @@ let close_block bt pts = if Proof.no_focused_goal pts then goto_current_focus pts else - let stack =get_stack pts in + let stack = + if Proof.is_done pts then + get_top_stack pts + else + get_stack pts + in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> (goto_current_focus pts) @@ -197,7 +203,7 @@ let close_block bt pts = | ET_Induction -> error "\"end induction\" expected." end | _,_ -> anomaly "Lonely suppose on stack." - + (* utility for suppose / suppose it is *) @@ -577,8 +583,8 @@ let instr_claim _thus st gls0 = let ninfo1 = {pm_stack= (if _thus then Focus_claim else Claim)::info.pm_stack} in tclTHENS (assert_postpone id st.st_it) - [tcl_change_info ninfo1; - thus_tac] gls0 + [thus_tac; + tcl_change_info ninfo1] gls0 (* tactics for assume *) @@ -1294,12 +1300,9 @@ let understand_my_constr c gls = let rec frob = function GEvar _ -> GHole (dummy_loc,QuestionMark Expand) | rc -> map_glob_constr frob rc in Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) -let set_refine,my_refine = -let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in -((fun tac -> refine:= tac), -(fun c gls -> - let oc = understand_my_constr c gls in - !refine oc gls)) +let my_refine c gls = + let oc = understand_my_constr c gls in + Refine.refine oc gls (* end focus/claim *) @@ -1438,12 +1441,16 @@ let rec postprocess pts instr = | Pcut _ | Psuffices _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> () | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ - | Pescape -> Proof.focus proof_cond 1 pts + | Pescape -> Decl_mode.focus pts | Pend (B_elim ET_Induction) -> begin let pfterm = List.hd (Proof.partial_proof pts) in let { it = gls ; sigma = sigma } = Proof.V82.subgoals pts in - let env = Goal.V82.env sigma (List.hd gls) in + let env = try + Goal.V82.env sigma (List.hd gls) + with Failure "hd" -> + Global.env () + in try Inductiveops.control_only_guard env pfterm; goto_current_focus_or_top pts @@ -1469,7 +1476,10 @@ let do_instr raw_instr pts = interp_proof_instr (get_its_info gl) sigma env glob_instr in Pfedit.by (tclTHEN (eval_instr instr) clean_tmp) else () end; - postprocess pts raw_instr.instr + postprocess pts raw_instr.instr; + (* spiwack: this should restore a compatible semantics with + v8.3 where we never stayed focused on 0 goal. *) + Decl_mode.maximal_unfocus pts let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index 0a2ab571ff..b27939b3ca 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -109,5 +109,3 @@ val init_tree: (int option * Declarations.recarg Rtree.t) array -> (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree - -val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit |