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`.

1 files changed, 27 insertions, 54 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 32dc4bb0f0..81c0a36f53 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -25,42 +25,26 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-let enable_unfocused_goal_printing = ref false
-let enable_goal_tags_printing = ref false
-let enable_goal_names_printing = ref false
-
-let should_tag() = !enable_goal_tags_printing
-let should_unfoc() = !enable_unfocused_goal_printing
-let should_gname() = !enable_goal_names_printing
-
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Unfocused"];
-      optread  = (fun () -> !enable_unfocused_goal_printing);
-      optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
-
 (* This is set on by proofgeneral proof-tree mode. But may be used for
    other purposes *)
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Goal";"Tags"];
-      optread  = (fun () -> !enable_goal_tags_printing);
-      optwrite = (fun b -> enable_goal_tags_printing:=b) }
-
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Goal";"Names"];
-      optread  = (fun () -> !enable_goal_names_printing);
-      optwrite = (fun b -> enable_goal_names_printing:=b) }
-
+let print_goal_tag_opt_name = ["Printing";"Goal";"Tags"]
+let should_tag =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:print_goal_tag_opt_name
+    ~value:false
+
+let should_unfoc =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Unfocused"]
+    ~value:false
+
+let should_gname =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Goal";"Names"]
+    ~value:false
 
 (**********************************************************************)
 (** Terms                                                             *)
@@ -407,17 +391,10 @@ let pr_context_limit_compact ?n env sigma =
 
 (* The number of printed hypothesis in a goal *)
 (* If [None], no limit *)
-let print_hyps_limit = ref (None : int option)
+let print_hyps_limit =
+  Goptions.declare_intopt_option_and_ref ~depr:false ~key:["Hyps";"Limit"]
 
-let () =
-  let open Goptions in
-  declare_int_option
-    { optdepr  = false;
-      optkey   = ["Hyps";"Limit"];
-      optread  = (fun () -> !print_hyps_limit);
-      optwrite = (fun x -> print_hyps_limit := x) }
-
-let pr_context_of env sigma = match !print_hyps_limit with
+let pr_context_of env sigma = match print_hyps_limit () with
   | None -> hv 0 (pr_context_limit_compact env sigma)
   | Some n -> hv 0 (pr_context_limit_compact ~n env sigma)
 
@@ -615,18 +592,14 @@ let print_evar_constraints gl sigma =
         str" with candidates:" ++ fnl () ++ hov 0 ppcandidates
     else mt ()
 
-let should_print_dependent_evars = ref false
-
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optkey   = ["Printing";"Dependent";"Evars";"Line"];
-      optread  = (fun () -> !should_print_dependent_evars);
-      optwrite = (fun v -> should_print_dependent_evars := v) }
+let should_print_dependent_evars =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Printing";"Dependent";"Evars";"Line"]
+    ~value:false
 
 let print_dependent_evars gl sigma seeds =
-  if !should_print_dependent_evars then
+  if should_print_dependent_evars () then
     let mt_pp = mt () in
     let evars = Evarutil.gather_dependent_evars sigma seeds in
     let evars_pp = Evar.Map.fold (fun e i s ->