diff options
| author | Maxime Dénès | 2017-10-03 15:00:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 15:00:20 +0200 |
| commit | 3fd0490c113432ae3fea6e6defa7b79acb36eae6 (patch) | |
| tree | 9c2c1aedd044f76001ae7317b22f0f2a66ee7982 | |
| parent | cd38c2030bbe024ce3c47d50d8cd961905263d43 (diff) | |
| parent | d14215865ec702897fd22a8d9272fede00cda11f (diff) | |
Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)
| -rw-r--r-- | ide/coqOps.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 9be70e6d38..0dd08293c8 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -480,8 +480,11 @@ object(self) | Message(lvl, loc, msg), Some (id,sentence) -> log_pp ?id Pp.(str "Msg " ++ msg); messages#push lvl msg + (* We do nothing here as for BZ#5583 *) + | Message(Error, loc, msg), None -> + log_pp Pp.(str "Error Msg without a sentence" ++ msg) | Message(lvl, loc, msg), None -> - log_pp Pp.(str "Msg " ++ msg); + log_pp Pp.(str "Msg without a sentence " ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n @@ -655,7 +658,7 @@ object(self) with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in loop tip [] in Coq.bind fill_queue process_queue - + method join_document = let next = function | Good _ -> |