From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 lib/feedback.mli | 102 ++++++++++++++++++++++---------------------------------
 1 file changed, 41 insertions(+), 61 deletions(-)

(limited to 'lib/feedback.mli')

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. *)
-- 
cgit v1.2.3