diff options
Diffstat (limited to 'kernel/names.ml')
-rw-r--r-- | kernel/names.ml | 18 |
1 files changed, 5 insertions, 13 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 |