aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/unicode.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/unicode.ml')
-rw-r--r--lib/unicode.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 1765e93dc..cfaa73cc1 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -168,6 +168,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 =