A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args

1 files changed, 16 insertions, 8 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index b04c7633a..711d2240b 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -206,12 +206,16 @@ let check_keyword str =
   in
   loop_symb (Stream.of_string str)
 
+let warn_unparsable_keyword =
+  CWarnings.create ~name:"unparsable-keyword" ~category:"parsing"
+         (fun (s,unicode) ->
+          strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
+                                  which will not be parsable." s unicode))
+            
 let check_keyword_to_add s =
   try check_keyword s
   with Error.E (UnsupportedUnicode unicode) ->
-    Flags.if_verbose Feedback.msg_warning
-      (strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \
-                               which will not be parsable." s unicode))
+    warn_unparsable_keyword (s,unicode)
 
 let check_ident str =
   let rec loop_id intail = parser
@@ -316,6 +320,14 @@ let rec number_or_index loc bp l len = parser
       | ['t';'h'] when check_no_char s -> njunk 2 s; check_gt3 loc l len
       | _ -> true, len
 
+let warn_comment_terminator_in_string =
+  CWarnings.create ~name:"comment-terminator-in-string" ~category:"parsing"
+         (fun () ->
+          (strbrk
+             "Not interpreting \"*)\" as the end of current \
+              non-terminated comment because it occurs in a \
+              non-terminated string of the comment."))
+
 (* If the string being lexed is in a comment, [comm_level] is Some i with i the
    current level of comments nesting. Otherwise, [comm_level] is None. *)
 let rec string loc ~comm_level bp len = parser
@@ -335,11 +347,7 @@ let rec string loc ~comm_level bp len = parser
         | [< '')'; s >] ->
             let () = match comm_level with
             | Some 0 ->
-                Feedback.msg_warning
-                  (strbrk
-                     "Not interpreting \"*)\" as the end of current \
-                      non-terminated comment because it occurs in a \
-                      non-terminated string of the comment.")
+	       warn_comment_terminator_in_string ~loc:!@loc ()
             | _ -> ()
             in
             let comm_level = Option.map pred comm_level in