From 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Jun 2016 18:51:32 +0200 Subject: [feedback] Remove unused tag on `Debug` level. IMO level indicators are not the proper place to store this information. --- lib/feedback.ml | 10 +++++----- lib/feedback.mli | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/feedback.ml b/lib/feedback.ml index d6f580fd16..74a18df6f8 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 diff --git a/lib/feedback.mli b/lib/feedback.mli index 50ffd22db9..690877897e 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -10,7 +10,7 @@ open Xml_datatype (* Old plain messages (used to be in Pp) *) type level = - | Debug of string + | Debug | Info | Notice | Warning -- cgit v1.2.3 From c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Jun 2016 00:41:33 +0200 Subject: [feedback] Add optional ?loc parameter to loggers. This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished. --- lib/feedback.ml | 26 +++++++++++++------------- lib/feedback.mli | 12 ++++++------ 2 files changed, 19 insertions(+), 19 deletions(-) (limited to 'lib') diff --git a/lib/feedback.ml b/lib/feedback.ml index 74a18df6f8..12b8b27ff4 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -51,7 +51,7 @@ let default_route = 0 open Pp open Pp_control -type logger = level -> std_ppcmds -> unit +type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) let msgnl strm = msgnl_with !std_ft strm @@ -84,7 +84,7 @@ let err_str = str "Error:" ++ spc () let make_body quoter info s = quoter (hov 0 (info ++ s)) (* Generic logger *) -let gen_logger dbg err level msg = match level with +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) | Notice -> msgnl msg @@ -93,10 +93,10 @@ let gen_logger dbg err level msg = match level with | Error -> msgnl_with !err_ft (make_body err err_str msg) (** Standard loggers *) -let std_logger = gen_logger (fun x -> x) (fun x -> x) +let std_logger = gen_logger (fun x -> x) (fun x -> x) (* Color logger *) -let color_terminal_logger level strm = +let color_terminal_logger ?loc level strm = let msg = Ppstyle.color_msg in match level with | Debug -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm @@ -117,11 +117,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 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_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 (** Feeders *) let feeder = ref ignore @@ -140,19 +140,19 @@ let feedback ?id ?route what = id = Option.default !feedback_id id; } -let feedback_logger lvl msg = +let feedback_logger ?loc lvl msg = feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, Richpp.richpp_of_pp msg)) (* Output to file *) -let ft_logger old_logger ft level mesg = +let ft_logger old_logger ft ?loc level mesg = let id x = x in match level with | 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 - | Error -> old_logger level mesg + | Warning -> old_logger ?loc level mesg + | Error -> old_logger ?loc level mesg let with_output_to_file fname func input = let old_logger = !logger in diff --git a/lib/feedback.mli b/lib/feedback.mli index 690877897e..7b293ae30b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -65,7 +65,7 @@ type feedback = { * Only one among state_id and edit_id can be provided. *) (** A [logger] takes a level plus a pretty printing doc and logs it *) -type logger = level -> Pp.std_ppcmds -> unit +type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit (** [set_logger l] makes the [msg_*] to use [l] for logging *) val set_logger : logger -> unit @@ -110,22 +110,22 @@ relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) -val msg_info : Pp.std_ppcmds -> unit +val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** Message that displays information, usually in verbose mode, such as [Foobar is defined] *) -val msg_notice : Pp.std_ppcmds -> unit +val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) -val msg_warning : Pp.std_ppcmds -> unit +val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** Message indicating that something went wrong, but without serious consequences. *) -val msg_error : Pp.std_ppcmds -> unit +val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** Message indicating that something went really wrong, though still recoverable; otherwise an exception would have been raised. *) -val msg_debug : Pp.std_ppcmds -> unit +val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** For debugging purposes *) -- cgit v1.2.3 From 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 16:05:25 +0200 Subject: [feedback] Allow messages to carry a location. The new warnings mechanism may which to forward a location to IDEs. This also makes sense for other message types. Next step is to remove redundant MsgError feedback type. --- lib/feedback.ml | 6 +++--- lib/feedback.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/feedback.ml b/lib/feedback.ml index 12b8b27ff4..c2b512e991 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -36,8 +36,8 @@ type feedback_content = | FileLoaded of string * string (* Extra metadata *) | Custom of Loc.t * string * xml - (* Old generic messages *) - | Message of level * Richpp.richpp + (* Generic messages *) + | Message of level * Loc.t option * Richpp.richpp type feedback = { id : edit_or_state_id; @@ -142,7 +142,7 @@ let feedback ?id ?route what = let feedback_logger ?loc lvl msg = feedback ~route:!feedback_route ~id:!feedback_id - (Message (lvl, Richpp.richpp_of_pp msg)) + (Message (lvl, loc, Richpp.richpp_of_pp msg)) (* Output to file *) let ft_logger old_logger ft ?loc level mesg = diff --git a/lib/feedback.mli b/lib/feedback.mli index 7b293ae30b..36fb3867fb 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -46,7 +46,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of level * Richpp.richpp + | Message of level * Loc.t option * Richpp.richpp type feedback = { id : edit_or_state_id; (* The document part concerned *) -- cgit v1.2.3 From 1053a1d4e8112ae78af86024073cf03c072d1a7c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 25 Jun 2016 16:14:23 +0200 Subject: [feedback] Remove `ErrorMsg` in favor of `Message Error`. The ErrorMsg datatype was introduced to allow locations in messages, however, it was redundant with error and used only in one place. We remove it in favor of a more uniform treatment of messages with location. This patch also removes the use of `Loc.ghost` in one place. Lightly tested. --- lib/feedback.ml | 1 - lib/feedback.mli | 3 +-- 2 files changed, 1 insertion(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/feedback.ml b/lib/feedback.ml index c2b512e991..bedbe226c2 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -24,7 +24,6 @@ type feedback_content = | Processed | Incomplete | Complete - | ErrorMsg of Loc.t * string | ProcessingIn of string | InProgress of int | WorkerStatus of string * string diff --git a/lib/feedback.mli b/lib/feedback.mli index 36fb3867fb..d72524e65f 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -31,7 +31,6 @@ type feedback_content = | Processed | Incomplete | Complete - | ErrorMsg of Loc.t * string (* STM optional data *) | ProcessingIn of string | InProgress of int @@ -45,7 +44,7 @@ type feedback_content = | FileLoaded of string * string (* Extra metadata *) | Custom of Loc.t * string * xml - (* Old generic messages *) + (* Generic messages *) | Message of level * Loc.t option * Richpp.richpp type feedback = { -- cgit v1.2.3