From e3c880264bf54083b962d41a4c6e1ef35ca464f2 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 17 Mar 2011 21:46:47 +0000
Subject: Goptions: repair Unset for int options

 Previous code was trying to do a bool write, and in case of error,
 a int write. But for compatibility reason, bool write error were
 turned into warnings, preventing Unset Foo Bar to work when
 Foo Bar is an int option.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13915 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/goptions.ml       | 40 +++++++++++++++++++++++++++++-----------
 library/goptions.mli      |  4 +++-
 toplevel/vernacentries.ml |  6 ++----
 3 files changed, 34 insertions(+), 16 deletions(-)

diff --git a/library/goptions.ml b/library/goptions.ml
index e047ab9a0..fbce68fad 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -303,19 +303,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 837174f58..d3e0ac1a6 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -149,10 +149,12 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
-(** The first argument is a locality flag. [Some true] = "Local", [Some false]="Global". *)
+(** The first argument is a locality flag.
+    [Some true] = "Local", [Some false]="Global". *)
 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ddd97dda5..faa21850d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -944,7 +944,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = true;
-      optname  = "level of inling duging functor application";
+      optname  = "the level of inling duging functor application";
       optkey   = ["Inline";"Level"];
       optread  = (fun () -> Some (Flags.get_inline_level ()));
       optwrite = (fun o ->
@@ -1026,9 +1026,7 @@ let vernac_set_option locality key = function
   | BoolValue b -> set_bool_option_value_gen locality key b
 
 let vernac_unset_option locality key =
-  try set_bool_option_value_gen locality key false
-  with _ ->
-  set_int_option_value_gen locality key None
+  unset_option_value_gen locality key
 
 let vernac_add_option key lv =
   let f = function
-- 
cgit v1.2.3