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

11 files changed, 229 insertions, 37 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 096305b98..c6c7b4242 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -87,8 +87,7 @@ let load_aux_file_for vfile =
   | End_of_file -> !h
   | Sys_error s | Scanf.Scan_failure s
   | Failure s | Invalid_argument s ->
-     Flags.if_verbose
-       Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+    Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
      empty_aux_file
 
 let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
new file mode 100644
index 000000000..68442bd7c
--- /dev/null
+++ b/lib/cWarnings.ml
@@ -0,0 +1,120 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+type status =
+  Disabled | Enabled | AsError
+
+type t = {
+  default : status;
+  category : string;
+  status : status;
+}
+
+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 ""
+
+let set_current_loc = (:=) current_loc
+
+let get_flags () = !flags
+
+let add_warning_in_category ~name ~category =
+  let ws =
+    try
+      Hashtbl.find categories category
+    with Not_found -> []
+  in
+  Hashtbl.replace categories category (name::ws)
+
+let create ~name ~category ?(default=Enabled) pp =
+  Hashtbl.add warnings name { default; category; status = default };
+  add_warning_in_category ~name ~category;
+  if default <> Disabled then
+    add_warning_in_category ~name ~category:"default";
+  fun ?loc x -> let w = Hashtbl.find warnings name in
+           match w.status with
+           | Disabled -> ()
+           | AsError ->
+              let loc = Option.default !current_loc loc in
+              Errors.user_err_loc (loc,"_",pp x)
+           | Enabled ->
+              let msg =
+                pp x ++ str " [" ++ str name ++ str "," ++
+                  str category ++ str "]"
+              in
+              let loc = Option.default !current_loc loc in
+              Feedback.msg_warning ~loc msg
+
+let warn_unknown_warning =
+  create ~name:"unknown-warning" ~category:"toplevel"
+         (fun name -> strbrk "Unknown warning name: " ++ str name)
+
+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
+
+let reset_default_warnings () =
+  Hashtbl.iter (fun name w ->
+                Hashtbl.replace warnings name { w with status = w.default })
+    warnings
+
+let set_all_warnings_status status =
+  Hashtbl.iter (fun name w ->
+                Hashtbl.replace warnings name { w with status })
+    warnings
+
+let parse_flag s =
+  if String.length s > 1 then
+    match String.get s 0 with
+    | '+' -> (AsError, String.sub s 1 (String.length s - 1))
+    | '-' -> (Disabled, String.sub s 1 (String.length s - 1))
+    | _ -> (Enabled, s)
+  else Errors.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 rec parse_warnings items =
+  List.iter (fun (status, name) -> set_warning_status ~name status) items
+
+(* For compatibility, we accept "none" *)
+let parse_flags s = 
+  if CString.equal s "none" then begin
+      Flags.make_warn false;
+      set_all_warnings_status Disabled
+    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
+    end
+
+let set_flags s =
+  flags := s; reset_default_warnings (); parse_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
new file mode 100644
index 000000000..351554284
--- /dev/null
+++ b/lib/cWarnings.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       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;
+}
+ *)
+
+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
diff --git a/lib/feedback.ml b/lib/feedback.ml
index bedbe226c..0ec3b2ebe 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -80,31 +80,33 @@ let info_str = mt ()
 let warn_str = str "Warning:" ++ spc ()
 let  err_str = str "Error:"   ++ spc ()
 
-let make_body quoter info s = quoter (hov 0 (info ++ s))
+let make_body quoter info ?loc s =
+  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+  quoter (hov 0 (loc ++ info ++ s))
 
 (* Generic logger *)
 let gen_logger dbg err ?loc level msg = match level with
-  | Debug   -> msgnl (make_body dbg  dbg_str msg)
-  | Info    -> msgnl (make_body dbg info_str msg)
+  | Debug   -> msgnl (make_body dbg  dbg_str ?loc msg)
+  | Info    -> msgnl (make_body dbg info_str ?loc msg)
+  (* XXX: What to do with loc here? *)
   | Notice  -> msgnl msg
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_str msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_str msg)
+               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
 
 (** Standard loggers *)
 let std_logger  = gen_logger (fun x -> x) (fun x -> x)
 
 (* Color logger *)
 let color_terminal_logger ?loc level strm =
-  let msg = Ppstyle.color_msg in
+  let msg  = Ppstyle.color_msg in
   match level with
-  | Debug   -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
-  | Info    -> msg !std_ft strm
-  | Notice  -> msg !std_ft strm
-  | Warning ->
-    let header = ("Warning", Ppstyle.warning_tag) in
-    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
-  | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm
+  | Debug   -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+  | Info    -> msg ?loc !std_ft strm
+  | Notice  -> msg ?loc !std_ft strm
+  | Warning -> Flags.if_warn (fun () ->
+               msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
+  | Error   -> msg ?loc ~header:("Error",   Ppstyle.error_tag)   !err_ft strm
 
 (* Rules for emacs:
    - Debug/info: emacs_quote_info
@@ -116,11 +118,11 @@ let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
 let logger       = ref std_logger
 let set_logger l = logger := l
 
-let msg_info    ?loc x = !logger Info x
-let msg_notice  ?loc x = !logger Notice x
-let msg_warning ?loc x = !logger Warning x
-let msg_error   ?loc x = !logger Error x
-let msg_debug   ?loc x = !logger Debug x
+let msg_info    ?loc x = !logger ?loc Info x
+let msg_notice  ?loc x = !logger ?loc Notice x
+let msg_warning ?loc x = !logger ?loc Warning x
+let msg_error   ?loc x = !logger ?loc Error x
+let msg_debug   ?loc x = !logger ?loc Debug x
 
 (** Feeders *)
 let feeder = ref ignore
diff --git a/lib/flags.ml b/lib/flags.ml
index ba19c7a63..13525165a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -172,7 +172,7 @@ let make_polymorphic_flag b =
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
-let warn = ref false
+let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
diff --git a/lib/lib.mllib b/lib/lib.mllib
index a6c09058d..4b13156d6 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,4 +1,5 @@
 Errors
+CWarnings
 Bigint
 Segmenttree
 Unicodetable
diff --git a/lib/pp.ml b/lib/pp.ml
index d07f01b90..f1eb4c059 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -197,6 +197,25 @@ let strbrk s =
     else if p = n then [] else [str (String.sub s p (n-p))]
   in List.fold_left (++) Glue.empty (aux 0 0)
 
+let pr_loc_pos loc =
+  if Loc.is_ghost loc then (str"<unknown>")
+  else
+    let loc = Loc.unloc loc in
+    int (fst loc) ++ str"-" ++ int (snd loc)
+
+let pr_loc loc =
+  if Loc.is_ghost loc then str"<unknown>"
+  else
+    let fname = loc.Loc.fname in
+    if CString.equal fname "" then
+      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+	   str"-" ++ int loc.ep ++ str":" ++ fnl ())
+    else
+      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+	   str":" ++ fnl())
+
 let ismt = is_empty
 
 (* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index a18744c37..3bd560812 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -166,6 +166,8 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
+val pr_loc : Loc.t -> std_ppcmds
+
 (** {6 Low-level pretty-printing functions with and without flush} *)
 
 (** FIXME: These ignore the logging settings and call [Format] directly *)
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index b068788c9..ecfaa822c 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -124,15 +124,16 @@ let init_color_output () =
   Format.pp_set_formatter_tag_functions !std_ft tag_handler;
   Format.pp_set_formatter_tag_functions !err_ft tag_handler
 
-let color_msg ?header ft strm =
+let color_msg ?loc ?header ft strm =
   let pptag = tag in
   let open Pp in
+  let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
   let strm = match header with
-    | None -> hov 0 strm
+    | None -> hov 0 (ploc ++ strm)
     | Some (h, t) ->
       let tag = Pp.Tag.inj t pptag in
       let h = Pp.tag tag (str h ++ str ":") in
-      hov 0 (h ++ spc () ++ strm)
+      hov 0 (ploc ++ h ++ spc () ++ strm)
   in
   pp_with ~pp_tag ft strm;
   Format.pp_print_newline ft ();
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 1cd701ed4..b07fcd5d4 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -48,7 +48,7 @@ val dump : unit -> (t * Terminal.style option) list
 
 val init_color_output : unit -> unit
 
-val color_msg : ?header:string * Format.tag ->
+val color_msg : ?loc:Loc.t -> ?header:string * Format.tag ->
   Format.formatter -> Pp.std_ppcmds -> unit
 (** {!color_msg ?header fmt pp} will format according to the tags
      defined in this file *)
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.")