From ecd2f83848ab06048d67189972e92657bffcc92d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 24 Nov 2011 19:12:48 +0000 Subject: 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 --- library/goptions.mli | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'library/goptions.mli') 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 -- cgit v1.2.3