diff options
| author | Pierre Boutillier | 2015-06-22 11:49:58 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2015-06-22 11:49:58 +0200 |
| commit | 6bec099f8487b9d3ec5c44079cf69d3474c73b91 (patch) | |
| tree | b23d8983fa887cc7e7255df455c64d5d54130787 /ide | |
| parent | 07e8eede6670a256a81d9d70133ebbeb64f45fe3 (diff) | |
| parent | 949d027ce8fa94b5c62f938b58c3f85d015b177b (diff) | |
Merge remote-tracking branch 'forge/v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq-ssreflect.lang | 1 | ||||
| -rw-r--r-- | ide/coq.lang | 1 | ||||
| -rw-r--r-- | ide/coqOps.ml | 2 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 16 |
4 files changed, 9 insertions, 11 deletions
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index 4c488ae89a..7cfc167018 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -190,6 +190,7 @@ <keyword>Eval</keyword> <keyword>Load</keyword> <keyword>Undo</keyword> + <keyword>Restart</keyword> <keyword>Goal</keyword> <keyword>Print</keyword> <keyword>Save</keyword> diff --git a/ide/coq.lang b/ide/coq.lang index 35dff85e62..c65432bdb7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -161,6 +161,7 @@ <keyword>Print</keyword> <keyword>Eval</keyword> <keyword>Undo</keyword> + <keyword>Restart</keyword> <keyword>Opaque</keyword> <keyword>Transparent</keyword> </context> diff --git a/ide/coqOps.ml b/ide/coqOps.ml index af728471f7..2387d65c30 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -655,8 +655,6 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") end; List.iter (fun { start } -> buffer#delete_mark start) seg; diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 1f3fa3ed36..69d460b016 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 |