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

1 files changed, 10 insertions, 4 deletions

diff --git a/library/goptions.mli b/library/goptions.mli
index ca2df0710..3b3651f39 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -122,13 +122,19 @@ type 'a option_sig = {
 
 (** When an option is declared synchronous ([optsync] is [true]), the output is
    a synchronous write function. Otherwise it is [optwrite] *)
+(** The [preprocess] function is triggered before setting the option. It can be
+    used to emit a warning on certain values, and clean-up the final value. *)
 
 type 'a write_function = 'a -> unit
 
-val declare_int_option   : int option option_sig -> int option write_function
-val declare_bool_option  : bool option_sig   -> bool write_function
-val declare_string_option: string option_sig -> string write_function
-val declare_stringopt_option: string option option_sig -> string option write_function
+val declare_int_option   : ?preprocess:(int option -> int option) ->
+                           int option option_sig -> int option write_function
+val declare_bool_option  : ?preprocess:(bool -> bool) ->
+                           bool option_sig   -> bool write_function
+val declare_string_option: ?preprocess:(string -> string) ->
+                           string option_sig -> string write_function
+val declare_stringopt_option: ?preprocess:(string option -> string option) ->
+                              string option option_sig -> string option write_function
 
 
 (** {6 Special functions supposed to be used only in vernacentries.ml } *)