diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-18 20:30:27 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-18 20:30:27 +0000 |
commit | 9e89bf92ee52004eaf4fc6491c623b9b7db1da2a (patch) | |
tree | 00b8a22e7b319059b14a5be43c0b580a17624a43 /library | |
parent | 2d3430f3a49d844fdbff5db8d706b372ffec7a17 (diff) |
Adding the type infrastructure to handle properly API management of options
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r-- | library/goptions.ml | 15 | ||||
-rw-r--r-- | library/goptions.mli | 12 |
2 files changed, 23 insertions, 4 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 7c522022f..75fba89fe 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -27,11 +27,18 @@ let nickname table = String.concat " " table let error_undeclared_key key = error ((nickname key)^": no table or option of this type") -type value = +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 +(* | IdentValue of global_reference *) (****************************************************************************) (* 1- Tables *) @@ -204,7 +211,7 @@ type 'a option_sig = { optread : unit -> 'a; optwrite : 'a -> unit } -type option_type = bool * (unit -> value) -> (value -> unit) +type option_type = bool * (unit -> option_value) -> (option_value -> unit) module OptionMap = Map.Make (struct type t = option_name let compare = compare end) @@ -348,7 +355,7 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s - | IdentValue r -> pr_global_env Idset.empty r +(* | IdentValue r -> pr_global_env Idset.empty r *) let print_option_value key = let (name,(_,read,_,_,_)) = get_option key in diff --git a/library/goptions.mli b/library/goptions.mli index d3e0ac1a6..1a89961ac 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -135,6 +135,18 @@ 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; +} + +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + val get_string_table : option_name -> < add : string -> unit; |