Revert "A new infrastructure for warnings."

This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.

I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.

11 files changed, 37 insertions, 225 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index c6c7b42429..096305b987 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -87,7 +87,8 @@ 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_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
+     Flags.if_verbose
+       Feedback.msg_warning 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
deleted file mode 100644
index 7436dfd147..0000000000
--- a/lib/cWarnings.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(************************************************************************)
-(*  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.filter_map_inplace (fun name w -> Some { w with status = w.default }) warnings
-
-let set_all_warnings_status status =
-  Hashtbl.filter_map_inplace (fun name w -> Some { 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 String.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 String.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
deleted file mode 100644
index 3515542840..0000000000
--- a/lib/cWarnings.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  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 0ec3b2ebe4..bedbe226c2 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -80,33 +80,31 @@ let info_str = mt ()
 let warn_str = str "Warning:" ++ spc ()
 let  err_str = str "Error:"   ++ spc ()
 
-let make_body quoter info ?loc s =
-  let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
-  quoter (hov 0 (loc ++ info ++ s))
+let make_body quoter info s = quoter (hov 0 (info ++ s))
 
 (* Generic logger *)
 let gen_logger dbg err ?loc level msg = match level with
-  | 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? *)
+  | Debug   -> msgnl (make_body dbg  dbg_str msg)
+  | Info    -> msgnl (make_body dbg info_str msg)
   | Notice  -> msgnl msg
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_str ?loc msg)
+               msgnl_with !err_ft (make_body err warn_str msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body err  err_str 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 ?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
+  | 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
 
 (* Rules for emacs:
    - Debug/info: emacs_quote_info
@@ -118,11 +116,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 ?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
+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
 
 (** Feeders *)
 let feeder = ref ignore
diff --git a/lib/flags.ml b/lib/flags.ml
index 13525165ab..ba19c7a63b 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 true
+let warn = ref false
 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 4b13156d60..a6c09058dd 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,5 +1,4 @@
 Errors
-CWarnings
 Bigint
 Segmenttree
 Unicodetable
diff --git a/lib/pp.ml b/lib/pp.ml
index 1cef69fcc3..d07f01b906 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -197,25 +197,6 @@ 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 String.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 3bd560812e..a18744c376 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -166,8 +166,6 @@ 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 ecfaa822c7..b068788c92 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -124,16 +124,15 @@ 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 ?loc ?header ft strm =
+let color_msg ?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 (ploc ++ strm)
+    | None -> hov 0 strm
     | Some (h, t) ->
       let tag = Pp.Tag.inj t pptag in
       let h = Pp.tag tag (str h ++ str ":") in
-      hov 0 (ploc ++ h ++ spc () ++ strm)
+      hov 0 (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 b07fcd5d4c..1cd701ed4e 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 : ?loc:Loc.t -> ?header:string * Format.tag ->
+val color_msg : ?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 b27918522c..8b53a11d67 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -18,10 +18,6 @@ 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
@@ -36,7 +32,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 warn_cannot_open_dir root;
+  else Feedback.msg_warning (str ("Cannot open " ^ root));
   List.rev !l
 
 (* Caching directory contents for efficient syntactic equality of file
@@ -89,22 +85,19 @@ 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 -> warn_ambiguous_file_name (filename,l,f)
+    | _ :: _ 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)
     | _ -> ()
     in
     (lpe, f)
@@ -149,16 +142,12 @@ 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 ->
-    warn_path_not_found ();
+    Feedback.msg_warning (str "system variable PATH not found");
     false
 
 let open_trapping_failure name =
@@ -166,14 +155,11 @@ 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 ->
-    warn_cannot_remove_file filename
+    Feedback.msg_warning
+      (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
 let error_corrupted file s =
   errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")