From ff58f3d68369e0e535a98326e53de782ff460096 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 May 2015 17:47:11 +0200 Subject: Granting wish #4221. --- ide/wg_ProofView.ml | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'ide/wg_ProofView.ml') diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b12d29d6c..a5faa60a8 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -162,12 +162,21 @@ 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 + let vb, pl = if total = 1 then "is", "" else "are", "s" in + let msg = Printf.sprintf "This subproof is complete, but there %s still %d \ + unfocused goal%s:\n\n" vb total pl + in + let () = view#buffer#insert msg in + 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