From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 library/goptions.ml  | 42 ++++++++++++++++++++++++++++++------------
 library/goptions.mli |  3 ++-
 2 files changed, 32 insertions(+), 13 deletions(-)

(limited to 'library')

diff --git a/library/goptions.ml b/library/goptions.ml
index bfd3b272..8cf560d5 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goptions.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: goptions.ml 13922 2011-03-21 16:25:18Z letouzey $ *)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -305,19 +305,37 @@ let set_option_value locality check_and_cast key v =
 
 let bad_type_error () = error "Bad type of value for this option."
 
-let set_int_option_value_gen locality = set_option_value  locality
-  (fun v -> function
-     | (IntValue _) -> IntValue v
-     | _ -> bad_type_error ())
+let check_int_value v = function
+  | IntValue _ -> IntValue v
+  | _ -> bad_type_error ()
+
+let check_bool_value v = function
+  | BoolValue _ -> BoolValue v
+  | _ -> bad_type_error ()
+
+let check_string_value v = function
+  | StringValue _ -> StringValue v
+  | _ -> bad_type_error ()
+
+let check_unset_value v = function
+  | BoolValue _ -> BoolValue false
+  | IntValue _ -> IntValue None
+  | _ -> bad_type_error ()
+
+(* Nota: For compatibility reasons, some errors are treated as
+   warning. This allows a script to refer to an option that doesn't
+   exist anymore *)
+
+let set_int_option_value_gen locality =
+  set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
-  try set_option_value locality (fun v -> function
-     | (BoolValue _) -> BoolValue v
-     | _ -> bad_type_error ()) key v
+  try set_option_value locality check_bool_value key v
+  with UserError (_,s) -> Flags.if_verbose msg_warning s
+let set_string_option_value_gen locality =
+  set_option_value locality check_string_value
+let unset_option_value_gen locality key =
+  try set_option_value locality check_unset_value key ()
   with UserError (_,s) -> Flags.if_verbose msg_warning s
-let set_string_option_value_gen locality = set_option_value locality
- (fun v -> function
-    | (StringValue _) -> StringValue v
-    | _ -> bad_type_error ())
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
diff --git a/library/goptions.mli b/library/goptions.mli
index d2f98cd2..2962b5ca 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: goptions.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: goptions.mli 13922 2011-03-21 16:25:18Z letouzey $ i*)
 
 (* This module manages customization parameters at the vernacular level     *)
 
@@ -157,6 +157,7 @@ val get_ref_table :
 val set_int_option_value_gen    : bool option -> option_name -> int option -> unit
 val set_bool_option_value_gen   : bool option -> option_name -> bool   -> unit
 val set_string_option_value_gen : bool option -> option_name -> string -> unit
+val unset_option_value_gen : bool option -> option_name -> unit
 
 val set_int_option_value    : option_name -> int option -> unit
 val set_bool_option_value   : option_name -> bool   -> unit
-- 
cgit v1.2.3