From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- ide/ideutils.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'ide/ideutils.mli') diff --git a/ide/ideutils.mli b/ide/ideutils.mli index e5307218..e32a4d9e 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,6 +52,11 @@ val pop_info : unit -> unit val clear_info : unit -> unit val flash_info : ?delay:int -> string -> unit +val xml_to_string : Richpp.richpp -> string + +val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> + #GText.buffer_skel -> Richpp.richpp -> unit + val set_location : (string -> unit) ref (* In win32, when a command-line is to be executed via cmd.exe @@ -64,9 +69,9 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Pp.message_level -> string -> unit +type logger = Feedback.level -> Richpp.richpp -> unit -val default_logger : Pp.message_level -> string -> unit +val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) (** {6 I/O operations} *) -- cgit v1.2.3