Merge PR #12038: Improve undeclared goption key messages.

Reviewed-by: SkySkimmer

8 files changed, 73 insertions, 39 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 1418407533..666ba8ee2e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -24,6 +24,10 @@ type option_value =
   | StringValue of string
   | StringOptValue of string option
 
+type table_value =
+  | StringRefValue of string
+  | QualidRefValue of qualid
+
 (** Summary of an option status *)
 type option_state = {
   opt_depr  : bool;
@@ -35,8 +39,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                                                                *)
@@ -184,6 +193,23 @@ end
 module MakeRefTable =
   functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
 
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+
+let iter_table f key lv =
+  let aux = function
+    | StringRefValue s ->
+       begin
+         try f.aux (get_string_table key) (Global.env()) s
+         with Not_found -> error_no_table_of_this_type ~kind:"string" key
+       end
+    | QualidRefValue locqid ->
+       begin
+         try f.aux (get_ref_table key) (Global.env()) locqid
+         with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
+       end
+  in
+  List.iter aux lv
+
 (****************************************************************************)
 (* 2- Flags.                                                              *)
 
@@ -387,9 +413,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..150954cbac 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -187,6 +187,10 @@ type option_value =
   | StringValue of string
   | StringOptValue of string option
 
+type table_value =
+  | StringRefValue of string
+  | QualidRefValue of qualid
+
 val set_option_value : ?locality:option_locality ->
   ('a -> option_value -> option_value) -> option_name -> 'a -> unit
 (** [set_option_value ?locality f name v] sets [name] to the result of
@@ -204,4 +208,7 @@ type option_state = {
 val get_tables : unit -> option_state OptionMap.t
 val print_tables : unit -> Pp.t
 
+type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
+val iter_table : iter_table_aux -> option_name -> table_value list -> unit
+
 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/g_vernac.mlg b/vernac/g_vernac.mlg
index 08ba49f92b..13145d3757 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -938,23 +938,23 @@ GRAMMAR EXTEND Gram
       | IDENT "Print"; IDENT "Table"; table = option_table ->
           { VernacPrintOption table }
 
-      | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
+      | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
         -> { VernacAddOption ([table;field], v) }
       (* A global value below will be hidden by a field above! *)
       (* In fact, we give priority to secondary tables *)
       (* No syntax for tertiary tables due to conflict *)
       (* (but they are unused anyway) *)
-      | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
+      | IDENT "Add"; table = IDENT; v = LIST1 table_value ->
           { VernacAddOption ([table], v) }
 
-      | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
+      | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
         -> { VernacMemOption (table, v) }
       | IDENT "Test"; table = option_table ->
           { VernacPrintOption table }
 
-      | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
+      | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
         -> { VernacRemoveOption ([table;field], v) }
-      | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
+      | IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
           { VernacRemoveOption ([table], v) } ]]
   ;
   query_command: (* TODO: rapprocher Eval et Check *)
@@ -1047,9 +1047,9 @@ GRAMMAR EXTEND Gram
       | n  = integer   -> { OptionSetInt n }
       | s  = STRING    -> { OptionSetString s } ] ]
   ;
-  option_ref_value:
-    [ [ id = global   -> { QualidRefValue id }
-      | s  = STRING   -> { StringRefValue s } ] ]
+  table_value:
+    [ [ id = global   -> { Goptions.QualidRefValue id }
+      | s  = STRING   -> { Goptions.StringRefValue s } ] ]
   ;
   option_table:
     [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7a2e6d8b03..36d79bfdb1 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -168,8 +168,8 @@ open Pputils
          keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b
 
   let pr_option_ref_value = function
-    | QualidRefValue id -> pr_qualid id
-    | StringRefValue s -> qs s
+    | Goptions.QualidRefValue id -> pr_qualid id
+    | Goptions.StringRefValue s -> qs s
 
   let pr_printoption table b =
     prlist_with_sep spc str table ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 044e479aeb..3926b91a55 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1554,26 +1554,11 @@ 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
-  in
-  try List.iter f lv with Not_found -> error_undeclared_key key
+let vernac_add_option = iter_table { aux = fun table -> table.add }
 
-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_remove_option = iter_table { aux = fun table -> table.remove }
 
-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_mem_option = iter_table { aux = fun table -> table.mem }
 
 let vernac_print_option key =
   try (get_ref_table key).print ()
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c32ac414ba..e46186288e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -121,10 +121,6 @@ type option_setting =
   | OptionSetInt of int
   | OptionSetString of string
 
-type option_ref_value =
-  | StringRefValue of string
-  | QualidRefValue of qualid
-
 (** Identifier and optional list of bound universes and constraints. *)
 
 type sort_expr = Sorts.family
@@ -406,9 +402,9 @@ type nonrec vernac_expr =
   | VernacSetStrategy of
       (Conv_oracle.level * qualid or_by_notation list) list
   | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting
-  | VernacAddOption of Goptions.option_name * option_ref_value list
-  | VernacRemoveOption of Goptions.option_name * option_ref_value list
-  | VernacMemOption of Goptions.option_name * option_ref_value list
+  | VernacAddOption of Goptions.option_name * Goptions.table_value list
+  | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
+  | VernacMemOption of Goptions.option_name * Goptions.table_value list
   | VernacPrintOption of Goptions.option_name
   | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
   | VernacGlobalCheck of constr_expr