[toplevel] Fix a couple of logical errors in error printing.

In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use
exceptions for error printing. However a couple of mistakes were
present in that commit:

- We wrongly absorbed the exception on `Vernac.compile`. However, it
  should be propagated as the caller will correctly print the error
  now. This introduced a critical bug as now `coqc` return the wrong
  exit status on error, breaking all sort of things.

- We printed parsing exceptions twice; now it is not necessary to
  print the exception in the parsing handler as it will be propagated.

I've checked this commit versus all previously reported bugs and it
seems to work; we should definitively add a test-suite case to check
that the exit code of `coqc` is correct, plus several other cases such
as bugs

https://coq.inria.fr/bugs/show_bug.cgi?id=5467
https://coq.inria.fr/bugs/show_bug.cgi?id=5485
https://coq.inria.fr/bugs/show_bug.cgi?id=5484

etc... See also PR #583

0 files changed, 0 insertions, 0 deletions