diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 9 |
1 files changed, 7 insertions, 2 deletions
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} *) |