Imported Upstream version 8.5~beta3+dfsg

1 files changed, 16 insertions, 7 deletions

diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b12d29d6..69d460b0 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+
 class type proof_view =
   object
     inherit GObj.widget
@@ -138,20 +140,22 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "No more subgoals."
     | [], [], [], _ :: _ ->
       (* A proof has been finished, but not concluded *)
-      view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
+      view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evars
+      List.iter iter evars;
+      view#buffer#insert "\nYou can use Grab Existential Variables."
     | [], [], _, _ ->
       (* The proof is finished, with the exception of given up goals. *)
-      view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n";
+      view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter given_up_goals
+      List.iter iter given_up_goals;
+      view#buffer#insert "\nYou need to go back and solve them."
     | [], _, _, _ ->
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
@@ -162,12 +166,17 @@ let display mode (view : #GText.view_skel) goals hints evars =
       List.iter iter shelved_goals
     | _, _, _, _ ->
       (* No foreground proofs, but still unfocused ones *)
-      view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
-      let iter goal =
+      let total = List.length bg in
+      let goal_str index = Printf.sprintf
+        "______________________________________(%d/%d)\n" index total
+      in
+      view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
+      let iter i goal =
+        let () = view#buffer#insert (goal_str (succ i)) in
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter bg
+      List.iteri iter bg
     end
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints