From d14215865ec702897fd22a8d9272fede00cda11f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Sep 2017 15:58:52 +0200 Subject: [ide] Avoid duplicate error printing (BZ#5583) See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds. --- ide/coqOps.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 9be70e6d3..0dd08293c 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 _ -> -- cgit v1.2.3