[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

1 files changed, 0 insertions, 2 deletions

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)