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, 9 insertions, 4 deletions

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