diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-24 15:58:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-29 11:47:03 +0200 |
| commit | d14215865ec702897fd22a8d9272fede00cda11f (patch) | |
| tree | 04b824e1fd17f042e1f3aacb83a4b06f5e2f1ab6 /ide/coqOps.ml | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
[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.
Diffstat (limited to 'ide/coqOps.ml')
| -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 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 _ -> |