Added a function to inspect current option state.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14727 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 14 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 7ba1d5189..d882ed944 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -27,18 +27,17 @@ let nickname table = String.concat " " table
 let error_undeclared_key key =
   error ((nickname key)^": no table or option of this type")
 
-type 'a option_state = {
-  opt_sync  : bool;
-  opt_name  : string;
-  opt_key   : option_name;
-  opt_value : 'a;
-}
-
 type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
-(*   | IdentValue  of global_reference *)
+
+type option_state = {
+  opt_sync  : bool;
+  opt_depr  : bool;
+  opt_name  : string;
+  opt_value : option_value;
+}
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
@@ -370,6 +369,19 @@ let print_option_value key =
 	     msg_option_value (name,s) ++ fnl ())
 
 
+let get_tables () =
+  let tables = !value_tab in
+  let fold key (name, depr, (sync,read,_,_,_)) accu =
+    let state = {
+      opt_sync = sync;
+      opt_name = name;
+      opt_depr = depr;
+      opt_value = read ();
+    } in
+    OptionMap.add key state accu
+  in
+  OptionMap.fold fold tables OptionMap.empty
+
 let print_tables () =
   let print_option key name value depr =
     let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
diff --git a/library/goptions.mli b/library/goptions.mli
index 37c03f1bf..685af53da 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -140,18 +140,20 @@ val declare_string_option: string option_sig -> string write_function
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)
 
-type 'a option_state = {
-  opt_sync  : bool;
-  opt_name  : string;
-  opt_key   : option_name;
-  opt_value : 'a;
-}
+module OptionMap : Map.S with type key = option_name
 
 type option_value =
   | BoolValue   of bool
   | IntValue    of int option
   | StringValue of string
 
+type option_state = {
+  opt_sync  : bool;
+  opt_depr  : bool;
+  opt_name  : string;
+  opt_value : option_value;
+}
+
 val get_string_table :
   option_name ->
     < add : string -> unit;
@@ -179,5 +181,6 @@ val set_string_option_value : option_name -> string -> unit
 
 val print_option_value : option_name -> unit
 
+val get_tables : unit -> option_state OptionMap.t
 val print_tables : unit -> unit