[options] New helper for creation of boolean options plus reference.

This makes setting the option outside of the synchronized summary impossible.

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 } *)