diff options
Diffstat (limited to 'lib/unicode.mli')
| -rw-r--r-- | lib/unicode.mli | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/lib/unicode.mli b/lib/unicode.mli index 00211164fb..2609e1968f 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,19 +8,17 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol +type status = Letter | IdentPart | Symbol | Unknown -exception Unsupported - -(** Classify a unicode char into 3 classes, or raise [Unsupported] *) +(** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status -(** Check whether a given string be used as a legal identifier. - - [None] means yes - - [Some (b,s)] means no, with explanation [s] and severity [b] *) +(** 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. *) val ident_refutation : string -> (bool * string) option -(** First char of a string, converted to lowercase *) +(** First char of a string, converted to lowercase + @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string (** Return [true] if all UTF-8 characters in the input string are just plain @@ -36,3 +34,9 @@ val ascii_of_ident : string -> string (** Validate an UTF-8 string *) val is_utf8 : string -> bool + +(** Return the length of a valid UTF-8 string. *) +val utf8_length : string -> int + +(** Variant of {!String.sub} for UTF-8 strings. *) +val utf8_sub : string -> int -> int -> string |