1 files changed, 83 insertions, 19 deletions

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 16286762..5160bd5b 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -9,27 +9,19 @@
 open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
-type message_level =
-  | Debug of string
+type level =
+  | Debug
   | Info
   | Notice
   | Warning
   | Error
 
-type message = {
-  message_level : message_level;
-  message_content : string;
-}
-
-val of_message : message -> xml
-val to_message : xml -> message
-val is_message : xml -> bool
-
 
 (** 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
+
 type route_id = int
 
 val default_route : route_id
@@ -39,7 +31,6 @@ type feedback_content =
   | Processed
   | Incomplete
   | Complete
-  | ErrorMsg of Loc.t * string
   (* STM optional data *)
   | ProcessingIn of string
   | InProgress of int
@@ -53,16 +44,89 @@ type feedback_content =
   | FileLoaded of string * string
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
-  (* Old generic messages *)
-  | Message of message
+  (* Generic messages *)
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
-  id : edit_or_state_id;       (* The document part concerned *)
+  id       : edit_or_state_id;  (* The document part concerned *)
   contents : feedback_content;  (* The payload *)
-  route : route_id;            (* Extra routing info *)
+  route    : route_id;          (* Extra routing info *)
 }
 
-val of_feedback : feedback -> xml
-val to_feedback : xml -> feedback
-val is_feedback : xml -> bool
+(** {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
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger    : logger
+
+
+(** [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
+
+(** [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
+
+(** {6 output functions}
+
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
+interfaces use the xml-like protocol this constraint can be
+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
+(** Message that displays information, usually in verbose mode, such as [Foobar
+    is defined] *)
+
+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 : ?loc:Loc.t -> Pp.std_ppcmds -> 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_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** For debugging purposes *)
+
+
+