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, 26 insertions, 12 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 8b53a11d6..b27918522 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -18,6 +18,10 @@ include Minisys
     depth-first search, with sons ordered as on the file system;
     warns if [root] does not exist *)
 
+let warn_cannot_open_dir =
+  CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
+  (fun dir -> str ("Cannot open directory " ^ dir))
+
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
@@ -32,7 +36,7 @@ let all_subdirs ~unix_path:root =
   in
   check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
-  else Feedback.msg_warning (str ("Cannot open " ^ root));
+  else warn_cannot_open_dir root;
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -85,19 +89,22 @@ let rec search paths test =
   | [] -> []
   | lpe :: rem -> test lpe @ search rem test
 
+let warn_ambiguous_file_name =
+  CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
+    (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
+                hov 0 (str "[ " ++
+                         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+                                               (fun (lpe,_) -> str lpe) l)
+                       ++ str " ];") ++ fnl () ++
+                str "loading " ++ str f)
+
+
 let where_in_path ?(warn=true) path filename =
   let check_and_warn l = match l with
   | [] -> raise Not_found
   | (lpe, f) :: l' ->
     let () = match l' with
-    | _ :: _ when warn ->
-      Feedback.msg_warning
-        (str filename ++ str " has been found in" ++ spc () ++
-          hov 0 (str "[ " ++
-            hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
-              (fun (lpe,_) -> str lpe) l)
-            ++ str " ];") ++ fnl () ++
-          str "loading " ++ str f)
+    | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
     | _ -> ()
     in
     (lpe, f)
@@ -142,12 +149,16 @@ let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
+let warn_path_not_found =
+  CWarnings.create ~name:"path-not-found" ~category:"filesystem"
+  (fun () -> str "system variable PATH not found")
+
 let is_in_system_path filename =
   try
     let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
     is_in_path lpath filename
   with Not_found ->
-    Feedback.msg_warning (str "system variable PATH not found");
+    warn_path_not_found ();
     false
 
 let open_trapping_failure name =
@@ -155,11 +166,14 @@ let open_trapping_failure name =
   with e when Errors.noncritical e ->
     errorlabstrm "System.open" (str "Can't open " ++ str name)
 
+let warn_cannot_remove_file =
+  CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
+  (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+
 let try_remove filename =
   try Sys.remove filename
   with e when Errors.noncritical e ->
-    Feedback.msg_warning
-      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+    warn_cannot_remove_file filename
 
 let error_corrupted file s =
   errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")