From 38a671f74857aec8e285a6a0bfcab876e3b9a133 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 13:26:53 +0100 Subject: Export the various option localities in the API. This prevents relying on an underspecified bool option argument. --- ide/ide_slave.ml | 2 +- library/goptions.ml | 39 +++++++++++++++++---------------------- library/goptions.mli | 15 ++++++++------- vernac/vernacentries.ml | 25 +++++++++++++++++-------- 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 -- cgit v1.2.3