diff options
| author | coqbot-app[bot] | 2021-01-27 08:34:33 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-27 08:34:33 +0000 |
| commit | 0c185094d40d10dc43f1432ef708a329fae25751 (patch) | |
| tree | f322ca666b1beb02e7a9d4d8195dc434f6593e4c | |
| parent | 7308d118879dcc603c45008c3d106ba3688f4e2b (diff) | |
| parent | 028342741eee445c44db2661b1c246623c96e01a (diff) | |
Merge PR #13785: [coqargs] use the standard option injection system for -w
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
| -rw-r--r-- | stm/stm.ml | 8 | ||||
| -rw-r--r-- | stm/stm.mli | 5 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 8 |
3 files changed, 12 insertions, 9 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 1c06c1efb7..0b00524bd5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2305,7 +2305,10 @@ end (* }}} *) (** STM initialization options: *) -type option_command = OptionSet of string option | OptionUnset +type option_command = + | OptionSet of string option + | OptionAppend of string + | OptionUnset type injection_command = | OptionInjection of (Goptions.option_name * option_command) @@ -2404,7 +2407,8 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let set_option = let open Goptions in function | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true - | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v + | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in let handle_injection = function | RequireInjection r -> require_file r diff --git a/stm/stm.mli b/stm/stm.mli index 097bcbe0ca..e0c33a309b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,7 +52,10 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -type option_command = OptionSet of string option | OptionUnset +type option_command = + | OptionSet of string option + | OptionAppend of string + | OptionUnset type injection_command = | OptionInjection of (Goptions.option_name * option_command) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index fbf3b4873b..c114c43e26 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -464,12 +464,8 @@ let parse_args ~help ~init arglist : t * string list = |"-w" | "-W" -> let w = next () in - if w = "none" then - (CWarnings.set_flags w; oval) - else - let w = CWarnings.get_flags () ^ "," ^ w in - CWarnings.set_flags (CWarnings.normalize_flags_string w); - oval + if w = "none" then add_set_option oval ["Warnings"] (Stm.OptionSet(Some w)) + else add_set_option oval ["Warnings"] (Stm.OptionAppend w) |"-bytecode-compiler" -> { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }} |