Adding an option -w to control Coq warning output.

For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.

6 files changed, 17 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 080b460a86..d2890f7402 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,10 @@ API
   All uses of unsafe_* functions should be eventually eliminated.
 
 
+Tools
+
+- Added an option -w to control the output of coqtop warnings.
+
 Changes from V8.5beta1 to V8.5beta2
 ===================================
 
diff --git a/lib/flags.ml b/lib/flags.ml
index f87dd5c2c8..313da0c5bd 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -160,7 +160,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/tools/coqc.ml b/tools/coqc.ml
index 31e0a0e0ad..aed229abc8 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -122,7 +122,7 @@ let parse_args () =
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
-      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0a14a19507..160e549afe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -114,6 +114,11 @@ let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
 
 let set_batch_mode () = batch_mode := true
 
+let set_warning = function
+| "all" -> make_warn true
+| "none" -> make_warn false
+| _ -> prerr_endline ("Error: all/none expected after option w"); exit 1
+
 let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
@@ -472,6 +477,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> toploop := Some (next ())
+    |"-w" -> set_warning (next ())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
@@ -505,7 +511,7 @@ let parse_args arglist =
     |"-notop" -> unset_toplevel_name ()
     |"-output-context" -> output_context := true
     |"-q" -> no_load_rc ()
-    |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false
     |"-quick" -> Flags.compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 94c1699c2a..50fb019f47 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -56,6 +56,10 @@ let print_usage_channel co command =
 \n  -v                     print Coq version and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
+\n  -quiet                 unset display of extra information (implies -w none)\
+\n  -w (all|none)          configure display of warnings\
+\n  -color (on|off|auto)   configure color output (only active through coqtop)\
+\n\
 \n  -q                     skip loading of rcfile\
 \n  -init-file f           set the rcfile to f\
 \n  -batch                 batch mode (exits just after arguments parsing)\
@@ -63,7 +67,6 @@ let print_usage_channel co command =
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
 \n  -emacs                 tells Coq it is executed under Emacs\
-\n  -color (on|off|auto)   configure color output (only active through coqtop)\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 96daf5075d..5418c60e94 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -257,7 +257,6 @@ let rec vernac_com verbosely checknav (loc,com) =
       else iraise (reraise, info)
 
 and read_vernac_file verbosely s =
-  Flags.make_warn verbosely;
   let checknav loc cmd =
     if is_navigation_vernac cmd && not (is_reset cmd) then
 	user_error loc "Navigation commands forbidden in files"