From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 28 Jun 2016 10:55:30 +0200 Subject: 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 --- lib/feedback.ml | 38 ++++++++++++++++++++------------------ 1 file changed, 20 insertions(+), 18 deletions(-) (limited to 'lib/feedback.ml') diff --git a/lib/feedback.ml b/lib/feedback.ml index bedbe226c..0ec3b2ebe 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -80,31 +80,33 @@ let info_str = mt () let warn_str = str "Warning:" ++ spc () let err_str = str "Error:" ++ spc () -let make_body quoter info s = quoter (hov 0 (info ++ s)) +let make_body quoter info ?loc s = + let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in + quoter (hov 0 (loc ++ info ++ s)) (* Generic logger *) let gen_logger dbg err ?loc level msg = match level with - | Debug -> msgnl (make_body dbg dbg_str msg) - | Info -> msgnl (make_body dbg info_str msg) + | 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? *) | Notice -> msgnl msg | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_str msg)) () - | Error -> msgnl_with !err_ft (make_body err err_str msg) + msgnl_with !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str ?loc 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 ~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 + | 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 (* Rules for emacs: - Debug/info: emacs_quote_info @@ -116,11 +118,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 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 +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 (** Feeders *) let feeder = ref ignore -- cgit v1.2.3