diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-10 13:24:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-14 14:17:11 +0100 |
| commit | 8fe6da32544ee73201f7c64b3dd45afb56c75b71 (patch) | |
| tree | 52c1c123d184fd4d32cc48243245c1012ee5afd5 /lib/cWarnings.ml | |
| parent | 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 (diff) | |
Fix bug in warnings: -w foo was silent when foo did not exist.
Diffstat (limited to 'lib/cWarnings.ml')
| -rw-r--r-- | lib/cWarnings.ml | 14 |
1 files changed, 10 insertions, 4 deletions
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" |