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

6 files changed, 118 insertions, 57 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 720f54606..68664d1ab 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
 
 let current_loc = ref Loc.ghost
-let flags = ref "default"
+let flags = ref ""
 
 let set_current_loc = (:=) current_loc
 
@@ -62,7 +62,7 @@ let set_warning_status ~name status =
   try
     let w = Hashtbl.find warnings name in 
     Hashtbl.replace warnings name { w with status = status }
-  with Not_found -> warn_unknown_warning name
+  with Not_found -> ()
 
 let reset_default_warnings () =
   Hashtbl.iter (fun name w ->
@@ -74,6 +74,13 @@ let set_all_warnings_status status =
                 Hashtbl.replace warnings name { w with status })
     warnings
 
+let set_category_status ~name status =
+  let names = Hashtbl.find categories name in
+  List.iter (fun name -> set_warning_status name status) names
+
+let is_all_keyword name = CString.equal name "all"
+let is_none_keyword s = CString.equal s "none"
+
 let parse_flag s =
   if String.length s > 1 then
     match String.get s 0 with
@@ -82,39 +89,94 @@ let parse_flag s =
     | _ -> (Enabled, s)
   else CErrors.error "Invalid warnings flag"
 
-let rec do_all_keyword = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     if CString.equal name "all" then
-       (set_all_warnings_status status; do_all_keyword items)
-     else item :: do_all_keyword items
-
-let rec do_categories = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     try
-       let names = Hashtbl.find categories name in
-       List.iter (fun name -> set_warning_status name status) names;
-       do_categories items
-     with Not_found -> item :: do_categories items
+let string_of_flag (status,name) =
+  match status with
+  | AsError -> "+" ^ name
+  | Disabled -> "-" ^ name
+  | Enabled -> name
+
+let string_of_flags flags =
+  String.concat "," (List.map string_of_flag flags)
+
+let set_status ~name status =
+  if is_all_keyword name then
+    set_all_warnings_status status
+  else
+    try
+      set_category_status ~name status
+    with Not_found ->
+         try
+           set_warning_status ~name status
+         with Not_found -> ()
+
+let split_flags s =
+  let reg = Str.regexp "[ ,]+" in Str.split reg s
+
+let check_warning ~silent (_status,name) =
+  is_all_keyword name ||
+  Hashtbl.mem categories name ||
+  Hashtbl.mem warnings name ||
+  (if not silent then warn_unknown_warning name; false)
+
+(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the
+    "all" flag, and reverses the list. *)
+let rec cut_before_all_rev acc = function
+  | [] -> acc
+  | (_status,name as w) :: warnings ->
+     cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings
+
+let cut_before_all_rev warnings = cut_before_all_rev [] warnings
+
+(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of
+    themselves or their categories, and reverses the list. *)
+let uniquize_flags_rev flags =
+  let rec aux acc visited = function
+    | (_,name as flag)::flags ->
+       if CString.Set.mem name visited then aux acc visited flags else
+         let visited =
+           try
+             let warnings = Hashtbl.find categories name in
+             CString.Set.union visited (CString.Set.of_list warnings)
+           with Not_found ->
+             visited
+         in
+         aux (flag::acc) (CString.Set.add name visited) flags
+    | [] -> acc
+  in aux [] CString.Set.empty flags
+
+(** [normalize_flags] removes unknown or redundant warnings. If [silent] is
+    true, it emits a warning when an unknown warning is met. *)
+let normalize_flags ~silent warnings =
+  let warnings = List.filter (check_warning ~silent) warnings in
+  let warnings = cut_before_all_rev warnings in
+  uniquize_flags_rev warnings
+
+let flags_of_string s = List.map parse_flag (split_flags s)
+
+let normalize_flags_string s =
+  if is_none_keyword s then s
+  else
+    let flags = flags_of_string s in
+    let flags = normalize_flags ~silent:false flags in
+    string_of_flags flags
 
 let rec parse_warnings items =
-  List.iter (fun (status, name) -> set_warning_status ~name status) items
+  CList.iter (fun (status, name) -> set_status ~name status) items
 
 (* For compatibility, we accept "none" *)
-let parse_flags s = 
-  if CString.equal s "none" then begin
+let parse_flags s =
+  if is_none_keyword s then begin
       Flags.make_warn false;
-      set_all_warnings_status Disabled
+      set_all_warnings_status Disabled;
+      "none"
     end
   else begin
       Flags.make_warn true;
-      let reg = Str.regexp "[ ,]+" in
-      let items = List.map parse_flag (Str.split reg s) in
-      let items = do_all_keyword items in
-      let items = do_categories items in
-      parse_warnings items
+      let flags = flags_of_string s in
+      let flags = normalize_flags ~silent:true flags in
+      parse_warnings flags;
+      string_of_flags flags
     end
 
 let set_flags s =
-  flags := s; reset_default_warnings (); parse_flags s
+  reset_default_warnings (); let s = parse_flags s in flags := s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index 351554284..3f6cee31b 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -6,29 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type status =
-  Disabled | Enabled | AsError
-
-(*
-type 'a repr = {
-  print : 'a -> Pp.std_ppcmds;
-  kind : string;
-  enabled : bool;
-}
- *)
+type status = Disabled | Enabled | AsError
 
 val set_current_loc : Loc.t -> unit
 
 val create : name:string -> category:string -> ?default:status ->
              ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
 
-(*
-val emit : 'a t -> 'a -> unit
-
-type any = Any : string * string * 'a repr -> any
-
-val dump : unit -> any list
- *)
-
 val get_flags : unit -> string
 val set_flags : string -> unit
+
+(** Cleans up a user provided warnings status string, e.g. removing unknown
+    warnings (in which case a warning is emitted) or subsumed warnings . *)
+val normalize_flags_string : string -> string
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
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 } *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e0d836df8..a33e7257a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -866,11 +866,16 @@ GEXTEND Gram
       | "Set"; table = option_table; v = option_value ->
         begin match v with
         | StringValue s ->
-          let (last, prefix) = List.sep_last table in
-          if String.equal last "Append" && not (List.is_empty prefix) then
-            VernacSetAppendOption (prefix, s)
+          (* We make a special case for warnings because appending is their
+          natural semantics *)
+          if CString.List.equal table ["Warnings"] then
+            VernacSetAppendOption (table, s)
           else
-            VernacSetOption (table, v)
+            let (last, prefix) = List.sep_last table in
+            if String.equal last "Append" && not (List.is_empty prefix) then
+              VernacSetAppendOption (prefix, s)
+            else
+              VernacSetOption (table, v)
         | _ -> VernacSetOption (table, v)
         end
       | "Set"; table = option_table ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4de1d9595..c03f183ff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1491,7 +1491,7 @@ let _ =
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
 let _ =
-  declare_string_option
+  declare_string_option ~preprocess:CWarnings.normalize_flags_string
     { optsync  = true;
       optdepr  = false;
       optname  = "warnings display";