aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-28 13:26:53 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-09 10:17:21 -0300
commit38a671f74857aec8e285a6a0bfcab876e3b9a133 (patch)
tree5622eb556afff6f4bef5eb9b190bc0e9ea27161a /library/goptions.mli
parent2069c0aec44a50031e33bcb9f7d86c1535ef6b84 (diff)
Export the various option localities in the API.
This prevents relying on an underspecified bool option argument.
Diffstat (limited to 'library/goptions.mli')
-rw-r--r--library/goptions.mli15
1 files changed, 8 insertions, 7 deletions
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