From 1ef197db161f49de5c9b0900de1114c8b6750625 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 7 Jun 2015 19:13:47 +0200
Subject: Fixing bug #4233: The command Restart is not fontified correctly.
---
ide/coq-ssreflect.lang | 1 +
ide/coq.lang | 1 +
2 files changed, 2 insertions(+)
(limited to 'ide')
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 @@
Eval
Load
Undo
+ Restart
Goal
Print
Save
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 @@
Print
Eval
Undo
+ Restart
Opaque
Transparent
--
cgit v1.2.3
From b831c43f592dff6cf307add90354c10f30bf5b58 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Jun 2015 16:29:50 +0200
Subject: Fix by Enrico on CoqIDE not locating errors anymore since
550da87456a.
---
ide/coqOps.ml | 2 --
1 file changed, 2 deletions(-)
(limited to 'ide')
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;
--
cgit v1.2.3
From 1e9ef2c64dcfa916ba3643b219040cd8dabfd48a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 19 Jun 2015 13:49:26 +0200
Subject: 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.
---
ide/wg_ProofView.ml | 16 +++++++---------
1 file changed, 7 insertions(+), 9 deletions(-)
(limited to 'ide')
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
--
cgit v1.2.3