diff options
Diffstat (limited to 'lib/unicode.ml')
| -rw-r--r-- | lib/unicode.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/unicode.ml b/lib/unicode.ml index 05998bb804..938e8f1a99 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -173,6 +173,13 @@ let next_utf8 s i = (c land 0x3F) lsl 6 + (d land 0x3F) else err () +let is_utf8 s = + let rec check i = + let (off, _) = next_utf8 s i in + check (i + off) + in + try check 0 with End_of_input -> true | Invalid_argument _ -> false + (* Check the well-formedness of an identifier *) let initial_refutation j n s = |
