Clean and fix definitions of options.

- Provide new helper functions in `Goptions` on the model of
  `declare_bool_option_and_ref`;

- Use these helper functions in many parts of the code base
  (encapsulates the corresponding references);

- Move almost all options from `declare_string_option` to
  `declare_stringopt_option` (only "Warnings" continue to use the
  former).  This means that these options now support `Unset` to get
  back to the default setting.  Note that there is a naming
  misalignment since `declare_int_option` is similar to
  `declare_stringopt_option` and supports `Unset`.  When "Warning" is
  eventually migrated to support `Unset` as well, we can remove
  `declare_string_option` and rename `declare_stringopt_option` to
  `declare_string_option`.

- For some vernac options and flags that have an equivalent
  command-line option or flag, implement it like the standard `-set`
  and `-unset`.

2 files changed, 100 insertions, 6 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 75eef5b411..73132868d7 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -296,6 +296,48 @@ let declare_stringopt_option =
     (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option."))
     (fun _ _ -> anomaly (Pp.str "async_option."))
 
+
+type 'a opt_decl = depr:bool -> key:option_name -> 'a
+
+let declare_int_option_and_ref ~depr ~key ~(value:int) =
+  let r_opt = ref value in
+  let optwrite v = r_opt := Option.default value v in
+  let optread () = Some !r_opt in
+  let _ = declare_int_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  fun () -> !r_opt
+
+let declare_intopt_option_and_ref ~depr ~key =
+  let r_opt = ref None in
+  let optwrite v = r_opt := v in
+  let optread () = !r_opt in
+  let _ = declare_int_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  optread
+
+let declare_nat_option_and_ref ~depr ~key ~(value:int) =
+  assert (value >= 0);
+  let r_opt = ref value in
+  let optwrite v =
+    let v = Option.default value v in
+    if v < 0 then
+      CErrors.user_err Pp.(str "This option expects a non-negative value.");
+    r_opt := v
+  in
+  let optread () = Some !r_opt in
+  let _ = declare_int_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  fun () -> !r_opt
+
 let declare_bool_option_and_ref ~depr ~key ~(value:bool) =
   let r_opt = ref value in
   let optwrite v = r_opt := v in
@@ -307,6 +349,39 @@ let declare_bool_option_and_ref ~depr ~key ~(value:bool) =
     } in
   optread
 
+let declare_string_option_and_ref ~depr ~key ~(value:string) =
+  let r_opt = ref value in
+  let optwrite v = r_opt := Option.default value v in
+  let optread () = Some !r_opt in
+  let _ = declare_stringopt_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  fun () -> !r_opt
+
+let declare_stringopt_option_and_ref ~depr ~key =
+  let r_opt = ref None in
+  let optwrite v = r_opt := v in
+  let optread () = !r_opt in
+  let _ = declare_stringopt_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  optread
+
+let declare_interpreted_string_option_and_ref ~depr ~key ~(value:'a) from_string to_string =
+  let r_opt = ref value in
+  let optwrite v = r_opt := Option.default value @@ Option.map from_string v in
+  let optread () = Some (to_string !r_opt) in
+  let _ = declare_stringopt_option {
+      optdepr = depr;
+      optkey = key;
+      optread; optwrite
+    } in
+  fun () -> !r_opt
+
 (* 3- User accessible commands *)
 
 (* Setting values of options *)
diff --git a/library/goptions.mli b/library/goptions.mli
index 8fcc258d47..336cae420c 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -104,9 +104,15 @@ end
 
 (** {6 Options. } *)
 
-(** These types and function are for declaring a new option of name [key]
-   and access functions [read] and [write]; the parameter [name] is the option name
-   used when printing the option value (command "Print Toto Titi." *)
+(** These types and function are for declaring a new option of name
+   [key] and access functions [read] and [write]; the parameter [name]
+   is the option name used when printing the option value (command
+   "Print Toto Titi."
+
+   The declare_*_option functions are low-level, to be used when
+   implementing complex option workflows, e.g. when setting one option
+   changes the value of another.  For most use cases, you should use
+   the helper functions declare_*_option_and_ref. *)
 
 type 'a option_sig = {
   optdepr    : bool;
@@ -118,7 +124,11 @@ type 'a option_sig = {
 }
 
 (** The [preprocess] function is triggered before setting the option. It can be
-    used to emit a warning on certain values, and clean-up the final value. *)
+    used to emit a warning on certain values, and clean-up the final value.
+
+    [declare_stringopt_option] should be preferred to [declare_string_option]
+    because it supports "Unset".
+    Only "Warnings" option is declared using the latter.*)
 
 val declare_int_option   : ?preprocess:(int option -> int option) ->
                            int option option_sig -> unit
@@ -129,9 +139,18 @@ 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
+(** Helpers to declare a reference controlled by an option. Read-only
    as to avoid races. *)
-val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool)
+type 'a opt_decl = depr:bool -> key:option_name -> 'a
+
+val declare_int_option_and_ref : (value:int -> (unit -> int)) opt_decl
+val declare_intopt_option_and_ref : (unit -> int option) opt_decl
+val declare_nat_option_and_ref : (value:int -> (unit -> int)) opt_decl
+val declare_bool_option_and_ref : (value:bool -> (unit -> bool)) opt_decl
+val declare_string_option_and_ref : (value:string -> (unit -> string)) opt_decl
+val declare_stringopt_option_and_ref : (unit -> string option) opt_decl
+val declare_interpreted_string_option_and_ref :
+  (value:'a -> (string -> 'a) -> ('a -> string) -> (unit -> 'a)) opt_decl
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)