aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-24 19:12:48 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-24 19:12:48 +0000
commitecd2f83848ab06048d67189972e92657bffcc92d (patch)
tree0bd4a599253ae6a3d68372d0d6650f2d99cb8b79 /library
parent2ed4b1e88e3e304c5146d74124d7057ac62c59a2 (diff)
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
Diffstat (limited to 'library')
-rw-r--r--library/goptions.ml28
-rw-r--r--library/goptions.mli15
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