summaryrefslogtreecommitdiff
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r--ide/ideutils.mli9
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} *)