Export the various option localities in the API.

This prevents relying on an underspecified bool option argument.

4 files changed, 43 insertions, 38 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0ba1b3a4f..9fe580091 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -340,7 +340,7 @@ let set_options options =
   | IntValue i -> Goptions.set_int_option_value name i
   | StringValue s -> Goptions.set_string_option_value name s
   | StringOptValue (Some s) -> Goptions.set_string_option_value name s
-  | StringOptValue None -> Goptions.unset_option_value_gen None name
+  | StringOptValue None -> Goptions.unset_option_value_gen name
   in
   List.iter iter options
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 5681421ca..5cd82e56f 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -229,11 +229,6 @@ let warn_deprecated_option =
          (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
                        strbrk " is deprecated")
 
-let get_locality = function
-  | Some true -> OptLocal
-  | Some false -> OptGlobal
-  | None -> OptDefault
-
 let declare_option cast uncast append ?(preprocess = fun x -> x)
   { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
@@ -250,9 +245,9 @@ let declare_option cast uncast append ?(preprocess = fun x -> x)
       let load_options i o = cache_options o in
       let subst_options (subst,obj) = obj in
       let discharge_options (_,(l,_,_ as o)) =
-        match l with OptLocal -> None | _ -> Some o in
+        match l with OptLocal -> None | (OptGlobal | OptDefault) -> Some o in
       let classify_options (l,_,_ as o) =
-        match l with OptGlobal -> Substitute o | _ -> Dispose in
+        match l with OptGlobal -> Substitute o | (OptLocal | OptDefault) -> Dispose in
       let options : option_locality * option_mod * _ -> obj =
         declare_object
           { (default_object (nickname key)) with
@@ -302,12 +297,12 @@ let warn_unknown_option =
                    (fun key -> strbrk "There is no option " ++
                                  str (nickname key) ++ str ".")
 
-let set_option_value locality check_and_cast key v =
+let set_option_value ?(locality = OptDefault) check_and_cast key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
   | Some (name, depr, (read,write,append)) ->
-    write (get_locality locality) (check_and_cast v (read ()))
+    write locality (check_and_cast v (read ()))
 
 let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
 
@@ -334,25 +329,25 @@ let check_unset_value v = function
    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 =
-  set_option_value locality check_bool_value key v
-let set_string_option_value_gen locality =
-  set_option_value locality check_string_value
-let unset_option_value_gen locality key =
-  set_option_value locality check_unset_value key ()
+let set_int_option_value_gen ?locality =
+  set_option_value ?locality check_int_value
+let set_bool_option_value_gen ?locality key v =
+  set_option_value ?locality check_bool_value key v
+let set_string_option_value_gen ?locality =
+  set_option_value ?locality check_string_value
+let unset_option_value_gen ?locality key =
+  set_option_value ?locality check_unset_value key ()
 
-let set_string_option_append_value_gen locality key v =
+let set_string_option_append_value_gen ?(locality = OptDefault) key v =
   let opt = try Some (get_option key) with Not_found -> None in
   match opt with
   | None -> warn_unknown_option key
   | Some (name, depr, (read,write,append)) ->
-    append (get_locality locality) (check_string_value v (read ()))
+    append locality (check_string_value v (read ()))
 
-let set_int_option_value = set_int_option_value_gen None
-let set_bool_option_value = set_bool_option_value_gen None
-let set_string_option_value = set_string_option_value_gen None
+let set_int_option_value opt v = set_int_option_value_gen opt v
+let set_bool_option_value opt v = set_bool_option_value_gen opt v
+let set_string_option_value opt v = set_string_option_value_gen opt v
 
 (* Printing options/tables *)
 
diff --git a/library/goptions.mli b/library/goptions.mli
index 31920b832..64015f42d 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -50,6 +50,8 @@ open Mod_subst
 
 type option_name = string list
 
+type option_locality = OptLocal | OptDefault | OptGlobal
+
 (** {6 Tables. } *)
 
 (** The functor [MakeStringTable] declares a table containing objects
@@ -150,13 +152,12 @@ val get_ref_table :
       mem : reference -> unit;
       print : unit >
 
-(** 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 set_string_option_append_value_gen : bool option -> option_name -> string -> unit
-val unset_option_value_gen : bool option -> option_name -> unit
+(** The first argument is a locality flag. *)
+val set_int_option_value_gen    : ?locality:option_locality -> option_name -> int option -> unit
+val set_bool_option_value_gen   : ?locality:option_locality -> option_name -> bool   -> unit
+val set_string_option_value_gen : ?locality:option_locality -> option_name -> string -> unit
+val set_string_option_append_value_gen : ?locality:option_locality -> option_name -> string -> unit
+val unset_option_value_gen : ?locality:option_locality -> 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/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4c9b41b21..3610e9da3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1539,18 +1539,27 @@ let vernac_set_opacity ~atts (v,l) =
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
-let vernac_set_option ~atts key = function
-  | StringValue s -> set_string_option_value_gen atts.locality key s
-  | StringOptValue (Some s) -> set_string_option_value_gen atts.locality key s
-  | StringOptValue None -> unset_option_value_gen atts.locality key
-  | IntValue n -> set_int_option_value_gen atts.locality key n
-  | BoolValue b -> set_bool_option_value_gen atts.locality key b
+let get_option_locality = function
+| Some true -> OptLocal
+| Some false -> OptGlobal
+| None -> OptDefault
+
+let vernac_set_option ~atts key opt =
+  let locality = get_option_locality atts.locality in
+  match opt with
+  | StringValue s -> set_string_option_value_gen ~locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
+  | StringOptValue None -> unset_option_value_gen ~locality key
+  | IntValue n -> set_int_option_value_gen ~locality key n
+  | BoolValue b -> set_bool_option_value_gen ~locality key b
 
 let vernac_set_append_option ~atts key s =
-  set_string_option_append_value_gen atts.locality key s
+  let locality = get_option_locality atts.locality in
+  set_string_option_append_value_gen ~locality key s
 
 let vernac_unset_option ~atts key =
-  unset_option_value_gen atts.locality key
+  let locality = get_option_locality atts.locality in
+  unset_option_value_gen ~locality key
 
 let vernac_add_option key lv =
   let f = function