diff options
author | 2014-06-25 17:04:35 +0200 | |
---|---|---|
committer | 2014-06-25 17:04:35 +0200 | |
commit | 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 (patch) | |
tree | 66ef0fdf8f9152d0740b1f875d80343bac1ae4af /lib/pp.mli | |
parent | 0a829ad04841d0973b22b4407b95f518276b66e7 (diff) |
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/
Diffstat (limited to 'lib/pp.mli')
-rw-r--r-- | lib/pp.mli | 24 |
1 files changed, 20 insertions, 4 deletions
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} *) |