From 9e89bf92ee52004eaf4fc6491c623b9b7db1da2a Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 18 Nov 2011 20:30:27 +0000
Subject: 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
---
 library/goptions.ml  | 15 +++++++++++----
 library/goptions.mli | 12 ++++++++++++
 2 files changed, 23 insertions(+), 4 deletions(-)

(limited to 'library')

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;
-- 
cgit v1.2.3