From 0ea7bdc2e315da9a0a8338e5099dfcaad0bac9ef Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Dec 2016 15:48:30 +0100
Subject: Fix #5242 - Dubious unsilenceable warning on invalid identifier

We make this warning configurable and disabled by default.
---
 kernel/names.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 9267a64d61..1eb9a31751 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,9 +34,15 @@ struct
 
   let hash = String.hash
 
+  let warn_invalid_identifier =
+    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
+                     ~default:CWarnings.Disabled
+                     (fun s -> str s)
+
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x)
+      if fatal then CErrors.error x else
+        if warn then warn_invalid_identifier x
     in
     Option.iter iter (Unicode.ident_refutation x)
 
-- 
cgit v1.2.3