aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/unicode.ml12
-rw-r--r--lib/unicode.mli1
2 files changed, 7 insertions, 6 deletions
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 0764531c1a..1765e93dcd 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -222,13 +222,13 @@ let lowercase_first_char s =
(** For extraction, we need to encode unicode character into ascii ones *)
+let is_basic_ascii s =
+ let ok = ref true in
+ String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
+ !ok
+
let ascii_of_ident s =
- let check_ascii s =
- let ok = ref true in
- String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
- !ok
- in
- if check_ascii s then s else
+ if is_basic_ascii s then s else
let i = ref 0 and out = ref "" in
begin try while true do
let j, n = next_utf8 s !i in
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 763123306f..2c6b0a7963 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -24,4 +24,5 @@ val ident_refutation : string -> (bool * string) option
val lowercase_first_char : string -> string
(** For extraction, turn a unicode string into an ascii-only one *)
+val is_basic_ascii : string -> bool
val ascii_of_ident : string -> string