From 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 25 Jun 2014 17:04:35 +0200
Subject: all coqide specific files moved into ide/

lib/interface split into:
 - lib/feedback
     subscribe-based feedback bus (also used by coqidetop)
 - ide/interface
     definition of coqide protocol messages
   lib/pp
     structured info/err/warn messages

lib/serialize split into:
 - lib/serialize
     generic xml serialization (list, pairs, int, loc, ...)
     used by coqide but potentially useful to other interfaces
 - ide/xmlprotocol
     serialization of protocol messages as in ide/interface

the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
---
 lib/pp.mli | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 635a149e8..fe11619c1 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -78,8 +78,19 @@ val close : unit -> std_ppcmds
 val tclose : unit -> std_ppcmds
 
 (** {6 Sending messages to the user} *)
+type message_level =
+  | Debug of string
+  | Info
+  | Notice
+  | Warning
+  | Error
 
-type logger = Interface.message_level -> std_ppcmds -> unit
+type message = {
+  message_level : message_level;
+  message_content : string;
+}
+
+type logger = message_level -> std_ppcmds -> unit
 
 val msg_info : std_ppcmds -> unit
 (** Message that displays information, usually in verbose mode, such as [Foobar
@@ -104,6 +115,11 @@ val std_logger : logger
 
 val set_logger : logger -> unit
 
+val of_message : message -> Xml_datatype.xml
+val to_message : Xml_datatype.xml -> message
+val is_message : Xml_datatype.xml -> bool
+
+
 (** {6 Feedback sent, even asynchronously, to the user interface} *)
 
 (* This stuff should be available to most of the system, line msg_* above.
@@ -116,10 +132,10 @@ val set_logger : logger -> unit
  * since the two phases are performed sequentially) *)
 
 val feedback :
-  ?state_id:Interface.state_id -> Interface.feedback_content -> unit
+  ?state_id:Feedback.state_id -> Feedback.feedback_content -> unit
 
-val set_id_for_feedback : Interface.edit_or_state_id -> unit
-val set_feeder : (Interface.feedback -> unit) -> unit
+val set_id_for_feedback : Feedback.edit_or_state_id -> unit
+val set_feeder : (Feedback.feedback -> unit) -> unit
 
 (** {6 Utilities} *)
 
-- 
cgit v1.2.3