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.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'lib/feedback.mli') diff --git a/lib/feedback.mli b/lib/feedback.mli index 690877897..7b293ae30 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