Revised behavior on ill-formed identifiers.

Namely: Replacing (currently deactivated) warning on illegal ident by
an error in strict mode and nothing in soft mode.

2 files changed, 8 insertions, 15 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 811b4a62a..f5b3f4e00 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,16 +34,8 @@ 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 warn_invalid_identifier x
-    in
+  let check_valid ?(strict=true) x =
+    let iter (fatal, x) = if fatal || strict then CErrors.error x in
     Option.iter iter (Unicode.ident_refutation x)
 
   let is_valid s = match Unicode.ident_refutation s with
@@ -52,15 +44,15 @@ struct
 
   let of_bytes s =
     let s = Bytes.to_string s in
-    check_soft s;
+    check_valid s;
     String.hcons s
 
   let of_string s =
-    let () = check_soft s in
+    let () = check_valid s in
     String.hcons s
 
   let of_string_soft s =
-    let () = check_soft ~warn:false s in
+    let () = check_valid ~strict:false s in
     String.hcons s
 
   let to_string id = id
diff --git a/kernel/names.mli b/kernel/names.mli
index be9b9422b..5b0163aa5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,11 +46,12 @@ sig
   val of_bytes : bytes -> t
   val of_string : string -> t
   (** Converts a string into an identifier.
-      @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
+      @raise UserError if the string is invalid as an identifier.
       @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val of_string_soft : string -> t
-  (** Same as {!of_string} except that no warning is ever issued.
+  (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted.
+      @raise UserError if the string is invalid as an UTF-8 string.
       @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
 
   val to_string : t -> string