diff options
| author | Pierre-Marie Pédrot | 2015-04-15 11:16:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-14 12:28:17 +0200 |
| commit | 81eb133d64ac81cbf6962d624b20c1aa55c2baae (patch) | |
| tree | d3e21aadfe30b89a6993d9ef9c9737630f88205f /toplevel | |
| parent | 4ad6855504db2ce15a474bd646e19151aa8142e2 (diff) | |
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.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | toplevel/usage.ml | 5 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 1 |
3 files changed, 11 insertions, 3 deletions
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" |