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.

3 files changed, 33 insertions, 8 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 *)