Simplifying the call to print_no_goals and not calling it when no goal

is ongoing.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 11 insertions, 27 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 7f27d3b9f0..fbb8759d1b 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -514,23 +514,15 @@ let get_current_pm_goal () =
   let gl = sig_it gls in
     prepare_goal sigma gl
 
-
 let get_current_goals () = 
     let pfts = get_pftreestate () in
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
     let sigma = Tacmach.evc_of_pftreestate pfts in
     List.map (prepare_goal sigma) gls
 
-let get_current_goals_nb () = 
-  try List.length (get_current_goals ()) with _ -> 0
-  
 let print_no_goal () =
-    let pfts = get_pftreestate () in
-    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
-    assert (gls = []);
-    let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
-    msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
-
+  (* Fall back on standard coq goal printer for completed goal printing *)
+  msg (pr_open_subgoals ())
 
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
   [("clear "^ident),("clear "^ident^".");
diff --git a/ide/coq.mli b/ide/coq.mli
index d9b27811e7..7ee95a4004 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -65,8 +65,6 @@ val get_current_goals : unit -> goal list
 
 val get_current_pm_goal : unit -> goal
 
-val get_current_goals_nb : unit -> int
-
 val print_no_goal : unit -> string
 
 val process_exn : exn -> string*(Util.loc option)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7ba267c31f..14a0fd0371 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -769,7 +769,7 @@ object(self)
     try
       proof_buffer#set_text "";
       match Decl_mode.get_current_mode () with
-          Decl_mode.Mode_none ->  proof_buffer#insert (Coq.print_no_goal ())
+          Decl_mode.Mode_none -> ()
         | Decl_mode.Mode_tactic ->   
             begin
               let s = Coq.get_current_goals () in
@@ -827,8 +827,7 @@ object(self)
         try
           proof_buffer#set_text "";
           match Decl_mode.get_current_mode () with
-              Decl_mode.Mode_none ->  
-                proof_buffer#insert (Coq.print_no_goal ())
+              Decl_mode.Mode_none -> ()
             | Decl_mode.Mode_tactic ->   
                 begin
                   match Coq.get_current_goals () with 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 37083eb461..b23f94a70f 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -274,7 +274,7 @@ let default_pr_goal g =
 	  pr_ltype_env_at_top env g.evar_concl
     else 
       (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
-      (str"thesis := "  ++ fnl ()),
+      (str "thesis := "  ++ fnl ()),
        pr_context_of env,
        pr_ltype_env_at_top env g.evar_concl
   in
@@ -336,11 +336,11 @@ let default_pr_subgoals close_cmd sigma = function
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in 
 	      if exl = [] then 
-		(str"Proof completed."  ++ fnl ())
+		(str"Proof completed." ++ fnl ())
 	      else
 		let pei = pr_evars_int 1 exl in
 		  (str "No more subgoals but non-instantiated existential " ++
-		     str "variables :"  ++fnl () ++ (hov 0 pei))
+		     str "variables:" ++ fnl () ++ (hov 0 pei))
       end
   | [g] ->
       let pg = default_pr_goal g in
@@ -386,20 +386,15 @@ let pr_goal     x = !printer_pr.pr_goal     x
 (* End abstraction layer                                              *)
 (**********************************************************************)
 
-let pr_subgoals_of_pfts pfts =
-  let close_cmd = Decl_mode.get_end_command pfts in
-  let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in 
-  let sigma = (top_goal_of_pftreestate pfts).sigma in
-    pr_subgoals close_cmd sigma gls
-      
 let pr_open_subgoals () =
   let pfts = get_pftreestate () in
+  let gls = fst (frontier (proof_of_pftreestate pfts)) in 
   match focus() with
     | 0 -> 
-	pr_subgoals_of_pfts pfts
+        let sigma = (top_goal_of_pftreestate pfts).sigma in
+        let close_cmd = Decl_mode.get_end_command pfts in
+        pr_subgoals close_cmd sigma gls
     | n -> 
-	let pf = proof_of_pftreestate pfts in
-	let gls = fst (frontier pf) in 
 	assert (n > List.length gls);
 	if List.length gls < 2 then 
 	  pr_subgoal n gls