From f4584f8a332c9077844e227c8b86d3cb1daf8b12 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 14 Sep 2015 16:40:28 +0200
Subject: Adding rich printing primitives.

---
 ide/ideutils.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ide/ideutils.mli')

diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1fb30e4d7..ea4c41ff0 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,6 +52,9 @@ val pop_info : unit -> unit
 val clear_info : unit -> unit
 val flash_info : ?delay:int -> string -> unit
 
+val insert_xml : ?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
-- 
cgit v1.2.3