diff options
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 65 |
1 files changed, 15 insertions, 50 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index 5160bd5bc1..dc104132a0 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -8,7 +8,7 @@ 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 +17,7 @@ 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 - +(** Coq "semantic" infos obtained during execution *) type route_id = int val default_route : route_id @@ -36,68 +32,41 @@ 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.std_ppcmds type feedback = { - id : edit_or_state_id; (* The document part concerned *) - contents : feedback_content; (* The payload *) + 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 - -(** [init_color_output ()] Enable color in the std_logger *) -val init_color_output : unit -> unit +(* The interpreter assignes an state_id to the ast, and feedbacks happening + * during interpretation are attached to it. + *) -(** [feedback_logger] will produce feedback messages instead IO events *) -val feedback_logger : logger -val emacs_logger : logger +(** [add_feeder f] adds a feeder listiner [f], returning its id *) +val add_feeder : (feedback -> unit) -> int - -(** [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 +(** [del_feeder fid] removes the feeder with id [fid] *) +val del_feeder : int -> 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 +val feedback : ?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 -> Stateid.t -> unit (** {6 output functions} @@ -126,7 +95,3 @@ val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** For debugging purposes *) - - - - |