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 --- stm/stm.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'stm') 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) -- cgit v1.2.3