From a615382472ee21e288bd7115be147415e465e897 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 16 Mar 2015 17:56:48 +0100 Subject: Declarative mode: plug the specialised printers back. It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces. --- plugins/decl_mode/decl_mode.ml | 15 +++++++++++++++ plugins/decl_mode/decl_mode.mli | 2 ++ plugins/decl_mode/g_decl_mode.ml4 | 24 ++++++++++++++++-------- printing/printer.ml | 32 +++++++++++++++++--------------- 4 files changed, 50 insertions(+), 23 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/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 2bd88d5aea..733476e856 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 @@ -130,7 +137,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 *) diff --git a/printing/printer.ml b/printing/printer.ml index 467395c92c..0d3a1c17e4 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -544,22 +544,25 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals else pr_rec 1 (g::l) in + (* Side effect! This has to be made more robust *) + let () = + match close_cmd with + | Some cmd -> msg_info cmd + | None -> () + in match goals with | [] -> begin - match close_cmd with - Some cmd -> cmd - | None -> - let exl = Evarutil.non_instantiated sigma in - if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + let exl = Evarutil.non_instantiated sigma in + if Evar.Map.is_empty exl then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int sigma 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end | [g] when not !Flags.print_emacs && pr_first -> let pg = default_pr_goal { it = g ; sigma = sigma; } in @@ -637,8 +640,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = with None -> str"" | Some s -> fnl () ++ str s) ++ fnl () in - msg_info end_cmd; - pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end -- cgit v1.2.3