From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- ide/wg_ProofView.ml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'ide/wg_ProofView.ml') 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 -- cgit v1.2.3