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, 23 insertions, 20 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 4aa3a2a21..7bead0b63 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -233,6 +233,11 @@ 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;
@@ -270,10 +275,7 @@ 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
-      Feedback.msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated")
-  in
+  let warn () = if depr then warn_deprecated_option key in
   let cread () = cast (read ()) in
   let cwrite v = warn (); write (uncast v) in
   let clwrite v = warn (); lwrite (uncast v) in
@@ -304,19 +306,22 @@ 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 (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 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 bad_type_error () = error "Bad type of value for this option."
 
@@ -346,13 +351,11 @@ 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 =
-  try set_option_value locality check_bool_value key v
-  with UserError (_,s) -> Feedback.msg_warning s
+  set_option_value locality check_bool_value key v
 let set_string_option_value_gen locality =
   set_option_value locality check_string_value
 let unset_option_value_gen locality key =
-  try set_option_value locality check_unset_value key ()
-  with UserError (_,s) -> Feedback.msg_warning s
+  set_option_value locality check_unset_value key ()
 
 let set_int_option_value = set_int_option_value_gen None
 let set_bool_option_value = set_bool_option_value_gen None