diff options
| author | Maxime Dénès | 2017-05-09 08:52:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-09 08:52:04 +0200 |
| commit | dc1bae5ff63ca71e80bf0ee19a643b5cb5b284b9 (patch) | |
| tree | 8068f080cbe12d79a4b09641c7a1c836a5d372f4 | |
| parent | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (diff) | |
| parent | d411a796341a138cacd72350715871f48f82920b (diff) | |
Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.
| -rw-r--r-- | toplevel/coqloop.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 5 |
2 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 9a4f476bd3..a80599cd57 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf = then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg +(* let print_toplevel_parse_error (e, info) buf = let loc = Loc.get_loc info in let lvl = Feedback.Error in let msg = CErrors.iprint (e, info) in print_error_for_buffer ?loc lvl msg buf - +*) end (*s The Coq prompt is the name of the focused proof, if any, and "Coq" @@ -260,7 +261,10 @@ let read_sentence sid input = with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); - TopErr.print_toplevel_parse_error reraise top_buffer; + (* The caller of read_sentence does the error printing now, this + should be re-enabled once we rely on the feedback error + printer again *) + (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise (** Coqloop Console feedback handler *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9f6f77ef1d..4fca4ea184 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -323,8 +323,5 @@ let compile verbosely f = let compile v f = ignore(CoqworkmgrApi.get 1); - begin - try compile v f - with any -> Topfmt.print_err_exn any - end; + compile v f; CoqworkmgrApi.giveback 1 |