Move new iter_table function to Goptions.

2 files changed, 28 insertions, 1 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index fbacd07226..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;
@@ -189,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.                                                              *)
 
diff --git a/library/goptions.mli b/library/goptions.mli
index 59b1667f5a..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,5 +208,7 @@ 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
+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