Merge PR #9754: Don't lose the warning name when warning becomes error.

Reviewed-by: ejgallego

1 files changed, 9 insertions, 12 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 0cf989e494..f199e2e608 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Pp
-
 type status =
   Disabled | Enabled | AsError
 
@@ -158,6 +156,10 @@ let set_flags s =
    warning flags string, because the warning being created might have been set
    already. *)
 let create ~name ~category ?(default=Enabled) pp =
+  let pp x = let open Pp in
+    pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
+    str category ++ str "]"
+  in
   Hashtbl.replace warnings name { default; category; status = default };
   add_warning_in_category ~name ~category;
   if default <> Disabled then
@@ -166,13 +168,8 @@ let create ~name ~category ?(default=Enabled) pp =
      new warning is now known. *)
   set_flags !flags;
   fun ?loc x ->
-           let w = Hashtbl.find warnings name in
-           match w.status with
-           | Disabled -> ()
-           | AsError -> CErrors.user_err ?loc (pp x)
-           | Enabled ->
-              let msg =
-                pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
-                  str category ++ str "]"
-              in
-              Feedback.msg_warning ?loc msg
+    let w = Hashtbl.find warnings name in
+    match w.status with
+    | Disabled -> ()
+    | AsError -> CErrors.user_err ?loc (pp x)
+    | Enabled -> Feedback.msg_warning ?loc (pp x)