From 2dbb54b1bc3967ee5d6e838cce8c56b88bd9477d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 7 Apr 2018 21:53:06 +0200 Subject: [warnings] Remove `set_current_loc` hack. Instead of the current hack that won't work as soon as we check some part of the document asynchronously, we make the warning processor recover a proper location if the warning doesn't have one attached. This is what CoqIDE does [but it queries it's own document model]. Fixes: #6172 --- toplevel/coqloop.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d0989cfcc..63b8b538a 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -272,6 +272,15 @@ let read_sentence ~state input = (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise +let extract_default_loc loc doc_id sid : Loc.t option = + match loc with + | Some _ -> loc + | None -> + try + let doc = Stm.get_doc doc_id in + Option.cata fst None Stm.(get_ast ~doc sid) + with _ -> loc + (** Coqloop Console feedback handler *) let coqloop_feed (fb : Feedback.feedback) = let open Feedback in match fb.contents with @@ -290,6 +299,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* Re-enable when we switch back to feedback-based error printing *) | Message (Error,loc,msg) -> () (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) + | Message (Warning,loc,msg) -> + let loc = extract_default_loc loc fb.doc_id fb.span_id in + TopErr.print_error_for_buffer ?loc Warning msg top_buffer | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer -- cgit v1.2.3