diff options
Diffstat (limited to 'plugins/decl_mode/g_decl_mode.ml4')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 57 |
1 files changed, 27 insertions, 30 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 03929b3b..d598e7c3 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic +open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in @@ -35,22 +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_raw_proof_instr _ _ _ instr = - Errors.anomaly (Pp.str "Cannot print a proof_instr") - (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller - dans cette direction - Ppdecl_proof.pr_proof_instr (Global.env()) instr - *) -let pr_proof_instr _ _ _ instr = Empty.abort instr -let pr_glob_proof_instr _ _ _ instr = Empty.abort instr +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 @@ -65,23 +64,18 @@ let vernac_decl_proof () = else begin Decl_proof_instr.go_to_proof_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end (* spiwack: some bureaucracy is not performed here *) let vernac_return () = begin Decl_proof_instr.return_from_tactic_mode () ; - Proof_global.set_proof_mode "Declarative" ; - Vernacentries.print_subgoals () + Proof_global.set_proof_mode "Declarative" end let vernac_proof_instr instr = - begin - Decl_proof_instr.proof_instr instr; - Vernacentries.print_subgoals () - end + Decl_proof_instr.proof_instr instr (* Before we can write an new toplevel command (see below) which takes a [proof_instr] as argument, we need to declare @@ -92,7 +86,7 @@ let vernac_proof_instr instr = (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = +let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = Genarg.make0 None "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode @@ -106,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 @@ -143,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 *) @@ -160,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 |