aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-04-01 13:44:54 +0200
committerGaëtan Gilbert2019-04-12 13:59:23 +0200
commit839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (patch)
tree37a4e9a4b9d291d630f63eb37f7307f91fe65d60 /ide
parent38b86f40b3e2c6ce0ea77c94cf0c48efbf7c9f13 (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.ml17
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