Stopping warning on unrecognized unicode character in notation (fixing #5136).

The warning was pointless since the notation was accepted and parsed
anyway.

We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).

For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".

1 files changed, 3 insertions, 9 deletions

diff --git a/lib/unicode.mli b/lib/unicode.mli
index 1f8bd44eee..2609e1968f 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -8,22 +8,16 @@
 
 (** Unicode utilities *)
 
-type status = Letter | IdentPart | Symbol
+type status = Letter | IdentPart | Symbol | Unknown
 
-(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *)
-exception Unsupported
-
-(** Classify a unicode char into 3 classes.
-    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
+(** Classify a unicode char into 3 classes or unknown. *)
 val classify : int -> status
 
 (** Return [None] if a given string can be used as a (Coq) identifier.
-    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity.
-    @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
+    Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *)
 val ident_refutation : string -> (bool * string) option
 
 (** First char of a string, converted to lowercase
-    @raise Unsupported if the input string contains unsupported UTF-8 characters.
     @raise Assert_failure if the input string is empty. *)
 val lowercase_first_char : string -> string