diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-24 18:51:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-25 17:17:44 +0200 |
| commit | 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 (patch) | |
| tree | b66cdd04db8d6f8ab35fa9eac96f3b58df9d6ce3 /lib/feedback.ml | |
| parent | 799b4028834c1b073db8349bf75e384750fed591 (diff) | |
[feedback] Remove unused tag on `Debug` level.
IMO level indicators are not the proper place to store this information.
Diffstat (limited to 'lib/feedback.ml')
| -rw-r--r-- | lib/feedback.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index d6f580fd1..74a18df6f 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -9,7 +9,7 @@ open Xml_datatype type level = - | Debug of string + | Debug | Info | Notice | Warning @@ -85,7 +85,7 @@ let make_body quoter info s = quoter (hov 0 (info ++ s)) (* Generic logger *) let gen_logger dbg err level msg = match level with - | Debug _ -> msgnl (make_body dbg dbg_str msg) + | Debug -> msgnl (make_body dbg dbg_str msg) | Info -> msgnl (make_body dbg info_str msg) | Notice -> msgnl msg | Warning -> Flags.if_warn (fun () -> @@ -99,7 +99,7 @@ let std_logger = gen_logger (fun x -> x) (fun x -> x) let color_terminal_logger level strm = let msg = Ppstyle.color_msg in match level with - | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm + | Debug -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm | Info -> msg !std_ft strm | Notice -> msg !std_ft strm | Warning -> @@ -121,7 +121,7 @@ let msg_info x = !logger Info x let msg_notice x = !logger Notice x let msg_warning x = !logger Warning x let msg_error x = !logger Error x -let msg_debug x = !logger (Debug "_") x +let msg_debug x = !logger Debug x (** Feeders *) let feeder = ref ignore @@ -148,7 +148,7 @@ let feedback_logger lvl msg = let ft_logger old_logger ft level mesg = let id x = x in match level with - | Debug _ -> msgnl_with ft (make_body id dbg_str mesg) + | Debug -> msgnl_with ft (make_body id dbg_str mesg) | Info -> msgnl_with ft (make_body id info_str mesg) | Notice -> msgnl_with ft mesg | Warning -> old_logger level mesg |