[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

4 files changed, 12 insertions, 8 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 92c86eaea..fda25a0a6 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -22,11 +22,8 @@ type t = {
 let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
 
-let current_loc = ref None
 let flags = ref ""
 
-let set_current_loc loc = current_loc := loc
-
 let get_flags () = !flags
 
 let add_warning_in_category ~name ~category =
@@ -170,7 +167,6 @@ let create ~name ~category ?(default=Enabled) pp =
   set_flags !flags;
   fun ?loc x ->
            let w = Hashtbl.find warnings name in
-           let loc = Option.append loc !current_loc in
            match w.status with
            | Disabled -> ()
            | AsError -> CErrors.user_err ?loc (pp x)
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index fa96b18c8..f97a53c4d 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -10,8 +10,6 @@
 
 type status = Disabled | Enabled | AsError
 
-val set_current_loc : Loc.t option -> unit
-
 val create : name:string -> category:string -> ?default:status ->
              ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit
 
diff --git a/stm/stm.ml b/stm/stm.ml
index ba0a2017a..30aa9ea06 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3013,7 +3013,6 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
        str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
        str "This is not supported yet, sorry.");
   let indentation, strlen = compute_indentation ?loc ontop in
-  CWarnings.set_current_loc loc;
   (* XXX: Classifiy vernac should be moved inside process transaction *)
   let clas = Vernac_classifier.classify_vernac ast in
   let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
@@ -3037,7 +3036,6 @@ let query ~doc ~at ~route s =
       while true do
         let { CAst.loc; v=ast } = parse_sentence ~doc at s in
         let indentation, strlen = compute_indentation ?loc at in
-        CWarnings.set_current_loc loc;
         let st = State.get_cached at in
         let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
         ignore(stm_vernac_interp ~route at st aast)
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