diff options
| author | Emilio Jesus Gallego Arias | 2020-04-28 15:47:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-28 15:47:38 +0200 |
| commit | 196b5e0d10db966529b3bd1d27014a9742c71d7c (patch) | |
| tree | 8b068c7e261a34bc0dca5034e21caec7f3b721ba /library/goptions.ml | |
| parent | 2c9854dec504140b6f813af294aa83b14b5af3e5 (diff) | |
| parent | 8215466a316a94589251fb0156586d68ea8b5c38 (diff) | |
Merge PR #12003: Improve error messages for Set and Unset commands.
Reviewed-by: ejgallego
Reviewed-by: jfehrle
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 666ba8ee2e..f096c5d749 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -425,38 +425,38 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let show_value_type = function - | BoolValue _ -> "bool" - | IntValue _ -> "int" - | StringValue _ -> "string" - | StringOptValue _ -> "string" - -let bad_type_error opt_value actual_type = +let bad_type_error ~expected ~got = 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 ".") + str "expected " ++ str expected ++ + str ", got " ++ str got ++ str ".") + +let error_flag () = + user_err Pp.(str "This is a flag. It does not take a value.") let check_int_value v = function + | BoolValue _ -> error_flag () | IntValue _ -> IntValue v - | optv -> bad_type_error optv "int" + | StringValue _ | StringOptValue _ -> + bad_type_error ~expected:"string" ~got:"int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | optv -> bad_type_error optv "bool" + | _ -> user_err Pp.(str "This is an option. A value must be provided.") let check_string_value v = function + | BoolValue _ -> error_flag () + | IntValue _ -> bad_type_error ~expected:"int" ~got:"string" | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | optv -> bad_type_error optv "nothing" + | StringValue _ -> user_err Pp.(str "This option does not support the \"Unset\" command.") (* Nota: For compatibility reasons, some errors are treated as - warning. This allows a script to refer to an option that doesn't + warnings. This allows a script to refer to an option that doesn't exist anymore *) let set_int_option_value_gen ?locality = |
