diff options
| -rw-r--r-- | library/goptions.ml | 14 | ||||
| -rw-r--r-- | library/goptions.mli | 1 | ||||
| -rw-r--r-- | test-suite/output/undeclared_key.out | 13 | ||||
| -rw-r--r-- | test-suite/output/undeclared_key.v | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 42 |
5 files changed, 55 insertions, 21 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 1418407533..fbacd07226 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -35,8 +35,13 @@ type option_state = { let nickname table = String.concat " " table +let error_no_table_of_this_type ~kind key = + user_err ~hdr:"Goptions" + (str ("There is no " ^ kind ^ "-valued table with this name: \"" ^ nickname key ^ "\".")) + let error_undeclared_key key = - user_err ~hdr:"Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err ~hdr:"Goptions" + (str ("There is no flag, option or table with this name: \"" ^ nickname key ^ "\".")) (****************************************************************************) (* 1- Tables *) @@ -387,9 +392,10 @@ let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string (* Setting values of options *) let warn_unknown_option = - CWarnings.create ~name:"unknown-option" ~category:"option" - (fun key -> strbrk "There is no option " ++ - str (nickname key) ++ str ".") + CWarnings.create + ~name:"unknown-option" ~category:"option" + (fun key -> strbrk "There is no flag or option with this name: \"" ++ + str (nickname key) ++ str "\".") let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in diff --git a/library/goptions.mli b/library/goptions.mli index 336cae420c..59b1667f5a 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -204,4 +204,5 @@ type option_state = { val get_tables : unit -> option_state OptionMap.t val print_tables : unit -> Pp.t +val error_no_table_of_this_type : kind:string -> option_name -> 'a val error_undeclared_key : option_name -> 'a diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out new file mode 100644 index 0000000000..ed768751fc --- /dev/null +++ b/test-suite/output/undeclared_key.out @@ -0,0 +1,13 @@ +The command has indeed failed with message: +There is no flag, option or table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +File "stdin", line 3, characters 0-22: +Warning: There is no flag or option with this name: "Search Blacklists". +[unknown-option,option] +The command has indeed failed with message: +There is no string-valued table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". diff --git a/test-suite/output/undeclared_key.v b/test-suite/output/undeclared_key.v new file mode 100644 index 0000000000..4134bc8bfa --- /dev/null +++ b/test-suite/output/undeclared_key.v @@ -0,0 +1,6 @@ +Fail Test Search Blacklists. +Fail Test Search Blacklist for foo. +Set Search Blacklists. +Fail Remove Search Blacklists "bar" foo. +Fail Remove Search Blacklist "bar" foo. +Fail Add Search Blacklist "bar" foo. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 044e479aeb..a6a38e5253 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1554,26 +1554,34 @@ let vernac_set_option ~locality table v = match v with vernac_set_option0 ~locality table v | _ -> vernac_set_option0 ~locality table v -let vernac_add_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).add (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid +(* We have to request twice the same polymorphic function as argument + because OCaml won't compute the same type for it in both cases. *) +let iter_table ~f ~g key lv = + let aux = function + | StringRefValue s -> + begin + try f (get_string_table key) (Global.env()) s + with Not_found -> error_no_table_of_this_type ~kind:"string" key + end + | QualidRefValue locqid -> + begin + try g (get_ref_table key) (Global.env()) locqid + with Not_found -> error_no_table_of_this_type ~kind:"qualid" key + end in - try List.iter f lv with Not_found -> error_undeclared_key key + List.iter aux lv -let vernac_remove_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).remove (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_add_option = + let aux table = table.add in + iter_table ~f:aux ~g:aux -let vernac_mem_option key lv = - let f = function - | StringRefValue s -> (get_string_table key).mem (Global.env()) s - | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid - in - try List.iter f lv with Not_found -> error_undeclared_key key +let vernac_remove_option = + let aux table = table.remove in + iter_table ~f:aux ~g:aux + +let vernac_mem_option = + let aux table = table.mem in + iter_table ~f:aux ~g:aux let vernac_print_option key = try (get_ref_table key).print () |