diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-11-02 15:57:19 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-02 16:05:07 +0100 |
commit | 2c5eef988f11979175de6d1983bc533ce18b1095 (patch) | |
tree | 52fd4bf2c873bbfc746485c474ca897b4a2bff78 /library/goptions.ml | |
parent | 7ba82ed9f595c7d93bd40846993c2447572a817a (diff) |
Fix various shortcomings of the warnings infrastructure.
- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
Diffstat (limited to 'library/goptions.ml')
-rw-r--r-- | library/goptions.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index dfb3c0e69..9dc0f4058 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -247,7 +247,7 @@ let get_locality = function | Some false -> OptGlobal | None -> OptDefault -let declare_option cast uncast append +let declare_option cast uncast append ?(preprocess = fun x -> x) { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in @@ -275,10 +275,11 @@ let declare_option cast uncast append subst_function = subst_options; discharge_function = discharge_options; classify_function = classify_options } in - (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v))) + (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) else (fun _ m v -> - match m with + let v = preprocess v in + match m with | OptSet -> write v | OptAppend -> write (append (read ()) v)) in |