1 files changed, 32 insertions, 7 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 053bba805d..508881cad8 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,8 +9,6 @@
 
 open Preferences
 
-exception Forbidden
-
 let warn_image () =
   let img = GMisc.image () in
   img#set_stock `DIALOG_WARNING;
@@ -31,13 +29,40 @@ let push_info,pop_info,clear_info =
   let size = ref 0 in
   (fun s -> incr size; ignore (status_context#push s)),
   (fun () -> decr size; status_context#pop ()),
-  (fun () -> for i = 1 to !size do status_context#pop () done; size := 0)
+  (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0)
 
 let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
-
+let xml_to_string xml =
+  let open Xml_datatype in
+  let buf = Buffer.create 1024 in
+  let rec iter = function
+  | PCData s -> Buffer.add_string buf s
+  | Element (_, _, children) ->
+    List.iter iter children
+  in
+  let () = iter (Richpp.repr xml) in
+  Buffer.contents buf
+
+let translate s = s
+
+let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg =
+  let open Xml_datatype in
+  let tag name =
+    let name = translate name in
+    match GtkText.TagTable.lookup buf#tag_table name with
+    | None -> raise Not_found
+    | Some tag -> new GText.tag tag
+  in
+  let rec insert tags = function
+  | PCData s -> buf#insert ~tags:(List.rev tags) s
+  | Element (t, _, children) ->
+    let tags = try tag t :: tags with Not_found -> tags in
+    List.iter (fun xml -> insert tags xml) children
+  in
+  insert tags (Richpp.repr msg)
 
 let set_location = ref  (function s -> failwith "not ready")
 
@@ -272,7 +297,7 @@ let textview_width (view : #GText.view_skel) =
   let char_width = GPango.to_pixels metrics#approx_char_width in
   pixel_width / char_width
 
-type logger = Pp.message_level -> string -> unit
+type logger = Pp.message_level -> Richpp.richpp -> unit
 
 let default_logger level message =
   let level = match level with
@@ -282,7 +307,7 @@ let default_logger level message =
   | Pp.Warning -> `WARNING
   | Pp.Error -> `ERROR
   in
-  Minilib.log ~level message
+  Minilib.log ~level (xml_to_string message)
 
 
 (** {6 File operations} *)