diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 15 | ||||
| -rw-r--r-- | library/goptions.mli | 3 |
2 files changed, 15 insertions, 3 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index bb9b4e29fc..98efb512ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -299,6 +299,18 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) +let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = + let r_opt = ref value in + let optwrite v = r_opt := v in + let optread () = !r_opt in + let _ = declare_bool_option { + optdepr = depr; + optname = name; + optkey = key; + optread; optwrite + } in + optread + (* 3- User accessible commands *) (* Setting values of options *) @@ -422,6 +434,3 @@ let print_tables () = (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () - - - diff --git a/library/goptions.mli b/library/goptions.mli index 900217e06b..b91553bf3c 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -131,6 +131,9 @@ val declare_string_option: ?preprocess:(string -> string) -> val declare_stringopt_option: ?preprocess:(string option -> string option) -> string option option_sig -> unit +(** Helper to declare a reference controlled by an option. Read-only + as to avoid races. *) +val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) |