diff options
| -rw-r--r-- | kernel/names.ml | 8 | ||||
| -rw-r--r-- | lib/util.ml | 10 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
3 files changed, 12 insertions, 8 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 735ab2899..de1d7cce8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -26,8 +26,12 @@ open Util type identifier = string -let check_ident_soft x = Option.iter Pp.warning (ident_refutation x) -let check_ident x = Option.iter Errors.error (ident_refutation x) +let check_ident_soft x = + Option.iter (fun (fatal,x) -> + if fatal then error x else Pp.msg_warning (str x)) + (ident_refutation x) +let check_ident x = + Option.iter (fun (_,x) -> Errors.error x) (ident_refutation x) let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id diff --git a/lib/util.ml b/lib/util.ml index 3a012acbb..85ff2cbc4 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -283,14 +283,14 @@ let initial_refutation j n s = | UnicodeLetter -> None | _ -> let c = String.sub s 0 j in - Some ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".") + Some (false,"Invalid character '"^c^"' at beginning of identifier \""^s^"\".") let trailing_refutation i j n s = match classify_unicode n with | UnicodeLetter | UnicodeIdentPart -> None | _ -> let c = String.sub s i j in - Some ("Invalid character '"^c^"' in identifier \""^s^"\".") + Some (false,"Invalid character '"^c^"' in identifier \""^s^"\".") let ident_refutation s = if s = ".." then None else try @@ -308,9 +308,9 @@ let ident_refutation s = end |x -> x with - | End_of_input -> Some "The empty string is not an identifier." - | UnsupportedUtf8 -> Some (s^": unsupported character in utf8 sequence.") - | Invalid_argument _ -> Some (s^": invalid utf8 sequence.") + | End_of_input -> Some (true,"The empty string is not an identifier.") + | UnsupportedUtf8 -> Some (true,s^": unsupported character in utf8 sequence.") + | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.") let lowercase_unicode = let tree = Segmenttree.make Unicodetable.to_lower in diff --git a/lib/util.mli b/lib/util.mli index 380f58eab..d98551823 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -61,7 +61,7 @@ type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol exception UnsupportedUtf8 -val ident_refutation : string -> string option +val ident_refutation : string -> (bool * string) option val classify_unicode : int -> utf8_status val lowercase_first_char_utf8 : string -> string val ascii_of_ident : string -> string |