diff options
| author | Gaëtan Gilbert | 2019-04-01 13:44:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-12 13:59:23 +0200 |
| commit | 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (patch) | |
| tree | 37a4e9a4b9d291d630f63eb37f7307f91fe65d60 /ide | |
| parent | 38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (diff) | |
Unify Set and Unset handling for options
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 10b8a2cdc5..543ff924bd 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [ ["Diffs"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacSetOption (_, o, StringValue _) - | VernacUnsetOption (_, o) -> coqide_known_option o + | VernacSetOption (_, o, OptionSetTrue) + | VernacSetOption (_, o, OptionSetString _) + | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -366,12 +366,13 @@ let get_options () = Goptions.OptionMap.fold fold table [] let set_options options = + let open Goptions in let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name + | BoolValue b -> set_bool_option_value name b + | IntValue i -> set_int_option_value name i + | StringValue s -> set_string_option_value name s + | StringOptValue (Some s) -> set_string_option_value name s + | StringOptValue None -> unset_option_value_gen name in List.iter iter options |
