From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- library/goptions.ml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index eb7bb5b4..dcbc46ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -172,7 +172,7 @@ end module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t - type key = reference + type key = qualid let compare = A.compare let table = ref_table let encode = A.encode @@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (name, depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") let check_int_value v = function | IntValue _ -> IntValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "bool" let check_string_value v = function | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | _ -> bad_type_error () + | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | _ -> bad_type_error () + | optv -> bad_type_error optv "nothing" (* Nota: For compatibility reasons, some errors are treated as warning. This allows a script to refer to an option that doesn't -- cgit v1.2.3