diff options
-rw-r--r-- | library/goptions.ml | 28 | ||||
-rw-r--r-- | library/goptions.mli | 15 |
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 |