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 --- lib/cWarnings.ml | 4 ---- lib/cWarnings.mli | 2 -- 2 files changed, 6 deletions(-) (limited to 'lib') 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 -- cgit v1.2.3