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

4 files changed, 56 insertions, 84 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 ->
diff --git a/printing/printer.mli b/printing/printer.mli
index 936426949c..8c633b5e79 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -19,9 +19,7 @@ open Notation_term
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
-val enable_unfocused_goal_printing: bool ref
-val enable_goal_tags_printing      : bool ref
-val enable_goal_names_printing     : bool ref
+val print_goal_tag_opt_name : string list
 
 (** Terms *)
 
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 3a6424ba9f..c78cc96a83 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -46,36 +46,37 @@ let write_color_enabled enabled =
 
 let color_enabled () = !term_color
 
-let diff_option = ref `OFF
+type diffOpt = DiffOff | DiffOn | DiffRemoved
 
-let read_diffs_option () = match !diff_option with
-| `OFF -> "off"
-| `ON -> "on"
-| `REMOVED -> "removed"
+let diffs_to_string = function
+  | DiffOff -> "off"
+  | DiffOn -> "on"
+  | DiffRemoved -> "removed"
 
-let write_diffs_option opt =
-  let enable opt =
-    if not (color_enabled ()) then
-      CErrors.user_err Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
-    else
-      diff_option := opt
-  in
-  match opt with
-  | "off" -> diff_option := `OFF
-  | "on" -> enable `ON
-  | "removed" -> enable `REMOVED
+
+let assert_color_enabled () =
+  if not (color_enabled ()) then
+    CErrors.user_err
+      Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
+
+let string_to_diffs = function
+  | "off" -> DiffOff
+  | "on" -> assert_color_enabled (); DiffOn
+  | "removed" -> assert_color_enabled (); DiffRemoved
   | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
 
-let () =
-  Goptions.(declare_string_option {
-    optdepr = false;
-    optkey = ["Diffs"];
-    optread = read_diffs_option;
-    optwrite = write_diffs_option
-  })
+let opt_name = ["Diffs"]
+
+let diff_option =
+  Goptions.declare_interpreted_string_option_and_ref
+    ~depr:false
+    ~key:opt_name
+    ~value:DiffOff
+    string_to_diffs
+    diffs_to_string
 
-let show_diffs () = !diff_option <> `OFF;;
-let show_removed () = !diff_option = `REMOVED;;
+let show_diffs () = match diff_option () with DiffOff -> false | _ -> true
+let show_removed () = match diff_option () with DiffRemoved -> true | _ -> false
 
 
 (* DEBUG/UNIT TEST *)
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 24b171770a..ea64439456 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -10,8 +10,8 @@
 
 (* diff options *)
 
-(** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
-val write_diffs_option : string -> unit
+(** Name of Diffs option *)
+val opt_name : string list
 
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool