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, 26 insertions, 25 deletions

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