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/goptions.ml | |
| 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/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 15 |
1 files changed, 11 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 |