diff options
| author | Enrico Tassi | 2014-03-19 10:11:22 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-03-26 14:07:36 +0100 |
| commit | 545ab8b8439366877b3b40b49c483b9b61c85298 (patch) | |
| tree | 92b22325e42d5bbe7bbf2f0e70995e103594c022 | |
| parent | a59b49b7fe5f41e092609a464ba1df6fba53911f (diff) | |
CoqIDE: better error reporting for Qed on incomplete proof
| -rw-r--r-- | ide/coqOps.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 18069c471b..ab1a86f78a 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -288,16 +288,14 @@ object(self) let all_tags = [ error_bg; to_process; incomplete; processed; unjustified; error ] in let tags = - (if has_flag sentence `PROCESSING then to_process else - if has_flag sentence `ERROR then error_bg else - processed) - :: + (if has_flag sentence `PROCESSING then [to_process] + else if has_flag sentence `ERROR then [error_bg] + else if has_flag sentence `INCOMPLETE then [incomplete] + else [processed]) @ (if [ `UNSAFE ] = sentence.flags then [unjustified] else []) in List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; - List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags; - if has_flag sentence `INCOMPLETE then - buffer#apply_tag incomplete ~start ~stop + List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags method private attach_tooltip sentence loc text = let start_sentence, stop_sentence, phrase = self#get_sentence sentence in |