diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 15 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_mode.mli | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 34 |
4 files changed, 40 insertions, 12 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 07df7c7f09..774c20c9ae 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -119,3 +119,18 @@ let get_last env = match Environ.named_context env with | (id,_,_)::_ -> id | [] -> error "no previous statement to use" + +let get_end_command pts = + match get_top_stack pts with + | [] -> "\"end proof\"" + | Claim::_ -> "\"end claim\"" + | Focus_claim::_-> "\"end focus\"" + | Suppose_case :: Per (et,_,_,_) :: _ | Per (et,_,_,_) :: _ -> + begin + match et with + Decl_expr.ET_Case_analysis -> + "\"end cases\" or start a new case" + | Decl_expr.ET_Induction -> + "\"end induction\" or start a new case" + end + | _ -> anomaly (Pp.str"lonely suppose") diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index e12c4c9237..fd7e15c150 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -72,6 +72,8 @@ val get_last: Environ.env -> Id.t (** [get_last] raises a [UserError] when it cannot find a previous statement in the environment. *) +val get_end_command : Proof.proof -> string + val focus : Proof.proof -> unit val unfocus : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index ab5282e791..9d0b7f3466 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1446,6 +1446,7 @@ let rec postprocess pts instr = anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend (B_elim ET_Case_analysis) -> goto_current_focus () + | Pend B_proof -> Proof_global.set_proof_mode "Classic" | Pend _ -> () let do_instr raw_instr pts = diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 2bd88d5aea..d598e7c3fa 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -36,13 +36,20 @@ let pr_goal gs = str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () -(* arnaud: rebrancher ça ? -let pr_open_subgoals () = - let p = Proof_global.give_me_the_proof () in - let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in - let close_cmd = Decl_mode.get_end_command p in - pr_subgoals close_cmd sigma goals -*) +let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = + match gll with + | [goal] when pr_first -> + pr_goal { Evd.it = goal ; sigma = sigma } + | _ -> + (* spiwack: it's not very nice to have to call proof global + here, a more robust solution would be to add a hook for + [Printer.pr_open_subgoals] in proof modes, in order to + compute the end command. Yet a more robust solution would be + to have focuses give explanations of their unfocusing + behaviour. *) + let p = Proof_global.give_me_the_proof () in + let close_cmd = Decl_mode.get_end_command p in + str "Subproof completed, now type " ++ str close_cmd ++ str "." let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr @@ -93,14 +100,16 @@ let proof_instr : raw_proof_instr Gram.entry = let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr -let classify_proof_instr _ = VtProofStep false, VtLater +let classify_proof_instr = function + | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow + | _ -> VtProofStep false, VtLater (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. The "-" indicates that the rule does not start with a distinguished string. *) -VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr - [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] +VERNAC proof_mode EXTEND ProofInstr + [ - proof_instr(instr) ] => [classify_proof_instr instr] -> [ vernac_proof_instr instr ] END (* It is useful to use GEXTEND directly to call grammar entries that have been @@ -130,7 +139,8 @@ let _ = (* We substitute the goal printer, by the one we built for the proof mode. *) Printer.set_printer_pr { Printer.default_printer_pr with - Printer.pr_goal = pr_goal } + Printer.pr_goal = pr_goal; + pr_subgoals = pr_subgoals; } end ; (* function [reset] goes back to No Proof Mode from Declarative Proof Mode *) @@ -147,7 +157,7 @@ VERNAC COMMAND EXTEND DeclProof [ "proof" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_decl_proof () ] END VERNAC COMMAND EXTEND DeclReturn -[ "return" ] => [ VtProofMode "Classic", VtNow ] -> [ vernac_return () ] +[ "return" ] => [ VtProofMode "Declarative", VtNow ] -> [ vernac_return () ] END let none_is_empty = function |