From 8fe6da32544ee73201f7c64b3dd45afb56c75b71 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 10 Nov 2016 13:24:54 +0100 Subject: Fix bug in warnings: -w foo was silent when foo did not exist. --- lib/cWarnings.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'lib/cWarnings.ml') diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 1a1944d61..cc2463e22 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -35,6 +35,10 @@ let add_warning_in_category ~name ~category = in Hashtbl.replace categories category (name::ws) +let refine_loc = function + | None when not (Loc.is_ghost !current_loc) -> Some !current_loc + | loc -> loc + let create ~name ~category ?(default=Enabled) pp = Hashtbl.add warnings name { default; category; status = default }; add_warning_in_category ~name ~category; @@ -44,15 +48,17 @@ let create ~name ~category ?(default=Enabled) pp = match w.status with | Disabled -> () | AsError -> - let loc = Option.default !current_loc loc in - CErrors.user_err_loc (loc,"_",pp x) + begin match refine_loc loc with + | Some loc -> CErrors.user_err_loc (loc,"_",pp x) + | None -> CErrors.errorlabstrm "_" (pp x) + end | Enabled -> let msg = pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ str category ++ str "]" in - let loc = Option.default !current_loc loc in - Feedback.msg_warning ~loc msg + let loc = refine_loc loc in + Feedback.msg_warning ?loc msg let warn_unknown_warning = create ~name:"unknown-warning" ~category:"toplevel" -- cgit v1.2.3