diff options
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 102 |
1 files changed, 41 insertions, 61 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 5160bd5b..64fdf372 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Xml_datatype -(* Old plain messages (used to be in Pp) *) +(* Legacy-style logging messages (used to be in Pp) *) type level = | Debug | Info @@ -17,11 +19,10 @@ type level = | Error -(** Coq "semantic" infos obtained during parsing/execution *) -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id +(** Document unique identifier for serialization *) +type doc_id = int +(** Coq "semantic" infos obtained during execution *) type route_id = int val default_route : route_id @@ -36,68 +37,42 @@ type feedback_content = | InProgress of int | WorkerStatus of string * string (* Generally useful metadata *) - | Goals of Loc.t * string | AddedAxiom | GlobRef of Loc.t * string * string * string * string | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string (* Extra metadata *) - | Custom of Loc.t * string * xml + | Custom of Loc.t option * string * xml (* Generic messages *) - | Message of level * Loc.t option * Richpp.richpp + | Message of level * Loc.t option * Pp.t type feedback = { - id : edit_or_state_id; (* The document part concerned *) - contents : feedback_content; (* The payload *) + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; (* The document part concerned *) route : route_id; (* Extra routing info *) + contents : feedback_content; (* The payload *) } (** {6 Feedback sent, even asynchronously, to the user interface} *) -(** Moved here from pp.ml *) - -(* Morally the parser gets a string and an edit_id, and gives back an AST. - * Feedbacks during the parsing phase are attached to this edit_id. - * The interpreter assignes an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id. - * 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 = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit - -(** [set_logger l] makes the [msg_*] to use [l] for logging *) -val set_logger : logger -> unit - -(** [std_logger] standard logger to [stdout/stderr] *) -val std_logger : logger +(* The interpreter assignes an state_id to the ast, and feedbacks happening + * during interpretation are attached to it. + *) -(** [init_color_output ()] Enable color in the std_logger *) -val init_color_output : unit -> unit +(** [add_feeder f] adds a feeder listiner [f], returning its id *) +val add_feeder : (feedback -> unit) -> int -(** [feedback_logger] will produce feedback messages instead IO events *) -val feedback_logger : logger -val emacs_logger : logger +(** [del_feeder fid] removes the feeder with id [fid] *) +val del_feeder : int -> unit - -(** [add_feeder] feeders observe the feedback *) -val add_feeder : (feedback -> unit) -> unit - -(** Prints feedback messages of kind Message(Debug,_) using msg_debug *) -val debug_feeder : feedback -> unit - -(** [feedback ?id ?route fb] produces feedback fb, with [route] and - [id] set appropiatedly, if absent, it will use the defaults set by - [set_id_for_feedback] *) -val feedback : - ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit +(** [feedback ?did ?sid ?route fb] produces feedback [fb], with + [route] and [did, sid] set appropiatedly, if absent, it will use + the defaults set by [set_id_for_feedback] *) +val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit (** [set_id_for_feedback route id] Set the defaults for feedback *) -val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit - -(** [with_output_to_file file f x] executes [f x] with logging - redirected to a file [file] *) -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b +val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit (** {6 output functions} @@ -109,24 +84,29 @@ relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) -val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_info : ?loc:Loc.t -> Pp.t -> unit (** Message that displays information, usually in verbose mode, such as [Foobar is defined] *) -val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_notice : ?loc:Loc.t -> Pp.t -> unit (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) -val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_warning : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. *) -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_error : ?loc:Loc.t -> Pp.t -> unit +[@@ocaml.deprecated "msg_error is an internal function and should not be \ + used unless you know what you are doing. Use \ + [CErrors.user_err] instead."] -val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) +val console_feedback_listener : Format.formatter -> feedback -> unit +(** Helper for tools willing to print to the feedback system *) - - +val warn_no_listeners : bool ref +(** The library will print a warning to the console if no listener is + available by default; ML-clients willing to use Coq without a + feedback handler should set this to false. *) |