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

3 files changed, 4 insertions, 15 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