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.

6 files changed, 71 insertions, 58 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 7bead0b63d..4aa3a2a21d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -233,11 +233,6 @@ with Not_found ->
 open Libobject
 open Lib
 
-let warn_deprecated_option =
-  CWarnings.create ~name:"deprecated-option" ~category:"deprecated"
-         (fun key -> str "Option" ++ spc () ++ str (nickname key) ++
-                       strbrk " is deprecated")
-
 let declare_option cast uncast
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
@@ -275,7 +270,10 @@ let declare_option cast uncast
     begin fun v -> add_anonymous_leaf (gdecl_obj v) end
   else write,write,write
   in
-  let warn () = if depr then warn_deprecated_option key in
+  let warn () =
+    if depr then
+      Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
+  in
   let cread () = cast (read ()) in
   let cwrite v = warn (); write (uncast v) in
   let clwrite v = warn (); lwrite (uncast v) in
@@ -306,22 +304,19 @@ let declare_stringopt_option =
 
 (* Setting values of options *)
 
-let warn_unknown_option =
-  CWarnings.create ~name:"unknown-option" ~category:"option"
-                   (fun key -> strbrk "There is no option " ++
-                                 str (nickname key) ++ str ".")
-
 let set_option_value locality check_and_cast key v =
-  let opt = try Some (get_option key) with Not_found -> None in
-  match opt with
-  | None -> warn_unknown_option key
-  | Some (name, depr, (_,read,write,lwrite,gwrite)) ->
-    let write = match locality with
-      | None -> write
-      | Some true -> lwrite
-      | Some false -> gwrite
-    in
-    write (check_and_cast v (read ()))
+  let (name, depr, (_,read,write,lwrite,gwrite)) =
+    try get_option key
+    with Not_found ->
+      errorlabstrm "Goptions.set_option_value"
+        (str "There is no option " ++ str (nickname key) ++ str ".")
+  in
+  let write = match locality with
+    | None -> write
+    | Some true -> lwrite
+    | Some false -> gwrite
+  in
+  write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option."
 
@@ -351,11 +346,13 @@ let check_unset_value v = function
 let set_int_option_value_gen locality =
   set_option_value locality check_int_value
 let set_bool_option_value_gen locality key v =
-  set_option_value locality check_bool_value key v
+  try set_option_value locality check_bool_value key v
+  with UserError (_,s) -> Feedback.msg_warning s
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
-  set_option_value locality check_unset_value key ()
+  try set_option_value locality check_unset_value key ()
+  with UserError (_,s) -> Feedback.msg_warning s
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None
diff --git a/library/libobject.ml b/library/libobject.ml
index 3e08b38b12..b12d2038ae 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -12,6 +12,18 @@ open Util
 
 module Dyn = Dyn.Make(struct end)
 
+(* The relax flag is used to make it possible to load files while ignoring
+   failures to incorporate some objects.  This can be useful when one
+   wants to work with restricted Coq programs that have only parts of
+   the full capabilities, but may still be able to work correctly for
+   limited purposes.  One example is for the graphical interface, that uses
+   such a limited Coq process to do only parsing.  It loads .vo files, but
+   is only interested in loading the grammar rule definitions. *)
+
+let relax_flag = ref false;;
+
+let relax b = relax_flag := b;;
+
 type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
@@ -102,16 +114,31 @@ let declare_object_full odecl =
   try declare_object_full odecl
   with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
 
+let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
+
 (* this function describes how the cache, load, open, and export functions
-   are triggered. *)
+   are triggered.  In relaxed mode, this function just return a meaningless
+   value instead of raising an exception when they fail. *)
 
 let apply_dyn_fun deflt f lobj =
   let tag = object_tag lobj in
-  let dodecl =
-    try Hashtbl.find cache_tab tag
-    with Not_found -> assert false
-  in
-  f dodecl
+  try
+    let dodecl =
+      try
+        Hashtbl.find cache_tab tag
+      with Not_found ->
+        failwith "local to_apply_dyn_fun" in
+    f dodecl
+  with
+    Failure "local to_apply_dyn_fun" ->
+      if not (!relax_flag || Hashtbl.mem missing_tab tag) then
+        begin
+          Feedback.msg_warning
+	    (Pp.str ("Cannot find library functions for an object with tag "
+                      ^ tag ^ " (a plugin may be missing)"));
+          Hashtbl.add missing_tab tag ()
+        end;
+      deflt
 
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
diff --git a/library/libobject.mli b/library/libobject.mli
index 51b9af059f..dbe0de8f8a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -107,6 +107,7 @@ val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
+val relax : bool -> unit
 
 (** {6 Debug} *)
 
diff --git a/library/library.ml b/library/library.ml
index cead907009..bc7723f481 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -271,12 +271,6 @@ exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
-let warn_several_object_files =
-  CWarnings.create ~name:"several-object-files" ~category:"require"
-         (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
-                            strbrk " instead of " ++ str vo ++
-                            strbrk " because it is more recent")
-
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
@@ -293,8 +287,9 @@ let locate_absolute_library dir =
   | [] -> raise LibNotFound
   | [file] -> file
   | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-    warn_several_object_files (vi, vo);
-    vi
+       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+         str vo ++ str " because it is more recent");
+       vi
   | [vo;vi] -> vo
   | _ -> assert false
 
@@ -316,7 +311,8 @@ let locate_qualified_library ?root ?(warn = true) qid =
     | [lpath, file] -> lpath, file
     | [lpath_vo, vo; lpath_vi, vi]
       when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-      warn_several_object_files (vi, vo);
+       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
+         str vo ++ str " because it is more recent");
        lpath_vi, vi
     | [lpath_vo, vo; _ ] -> lpath_vo, vo
     | _ -> assert false
@@ -757,7 +753,7 @@ let save_library_to ?todo dir f otab =
 	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = Feedback.msg_notice (str "Removed file " ++ str f') in
+    let () = Feedback.msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 6f4d79430d..33c0f41e17 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -50,13 +50,6 @@ let remove_load_path dir =
   let filter p = not (String.equal p.path_physical dir) in
   load_paths := List.filter filter !load_paths
 
-let warn_overriding_logical_loadpath =
-  CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath"
-         (fun (phys_path, old_path, coq_path) ->
-          str phys_path ++ strbrk " was previously bound to " ++
-            pr_dirpath old_path ++ strbrk "; it is remapped to " ++
-            pr_dirpath coq_path)
-
 let add_load_path phys_path coq_path ~implicit =
   let phys_path = CUnix.canonical_path_name phys_path in
   let filter p = String.equal p.path_physical phys_path in
@@ -79,8 +72,10 @@ let add_load_path phys_path coq_path ~implicit =
         let () =
           (* Do not warn when overriding the default "-I ." path *)
           if not (DirPath.equal old_path Nameops.default_root_prefix) then
-          warn_overriding_logical_loadpath (phys_path, old_path, coq_path)
-        in
+            Feedback.msg_warning
+              (str phys_path ++ strbrk " was previously bound to " ++
+                 pr_dirpath old_path ++ strbrk "; it is remapped to " ++
+                 pr_dirpath coq_path) in
         true in
     if replace then
       begin
diff --git a/library/nametab.ml b/library/nametab.ml
index f533bc7914..db902d625b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -82,14 +82,6 @@ module Make (U : UserName) (E : EqualityType) : NAMETREE
 struct
   type elt = E.t
 
-  (* A name became inaccessible, even with absolute qualification.
-     Example:
-     Module F (X : S). Module X.
-     The argument X of the functor F is masked by the inner module X.
-   *)
-  let masking_absolute n =
-    Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"))
-
   type user_name = U.t
 
   type path_status =
@@ -127,7 +119,9 @@ struct
 	      | Absolute (n,_) ->
 		  (* This is an absolute name, we must keep it
 		     otherwise it may become unaccessible forever *)
-                masking_absolute n; tree.path
+		    Feedback.msg_warning (str ("Trying to mask the absolute name \""
+			     ^ U.to_string n ^ "\"!"));
+		  tree.path
 	      | Nothing
 	      | Relative _ -> Relative (uname,o)
           else tree.path
@@ -150,6 +144,7 @@ struct
 	  | Nothing
 	  | Relative _ -> mktree (Absolute (uname,o)) tree.map
 
+
 let rec push_exactly uname o level tree = function
 | [] ->
   anomaly (Pp.str "Prefix longer than path! Impossible!")
@@ -160,7 +155,9 @@ let rec push_exactly uname o level tree = function
         | Absolute (n,_) ->
             (* This is an absolute name, we must keep it
                 otherwise it may become unaccessible forever *)
-            masking_absolute n; tree.path
+              Feedback.msg_warning (str ("Trying to mask the absolute name \""
+                        ^ U.to_string n ^ "\"!"));
+            tree.path
         | Nothing
         | Relative _ -> Relative (uname,o)
     in