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.

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