diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-06-19 13:49:26 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-06-19 13:49:26 +0200 |
commit | 1e9ef2c64dcfa916ba3643b219040cd8dabfd48a (patch) | |
tree | 4c42235cf5a29b4fa52609ba6411500751ff9564 /ide | |
parent | 03d1fa42c17896cb9d767b509e05bd0db78cb7d2 (diff) |
Make end-of-proof output consistent across toplevels.
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
Diffstat (limited to 'ide')
-rw-r--r-- | ide/wg_ProofView.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 1f3fa3ed3..69d460b01 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -140,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"; @@ -168,11 +170,7 @@ let display mode (view : #GText.view_skel) goals hints evars = 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 + 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 |