1 files changed, 50 insertions, 24 deletions

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 0330b8eff..3d0cd46cd 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,10 @@ class type message_view =
     inherit GObj.widget
     method connect : message_view_signals
     method clear : unit
-    method add : Richpp.richpp -> unit
+    method add : Pp.std_ppcmds -> unit
     method add_string : string -> unit
-    method set : Richpp.richpp -> unit
+    method set : Pp.std_ppcmds -> unit
+    method refresh : bool -> unit
     method push : Ideutils.logger
       (** same as [add], but with an explicit level instead of [Notice] *)
     method buffer : GText.buffer
@@ -57,46 +58,71 @@ let message_view () : message_view =
   let () = view#set_left_margin 2 in
   view#misc#show ();
   let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed cb in
-  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
+  let _ = background_color#connect#changed ~callback:cb in
+  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
   let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in
   stick text_font view cb;
-  object (self)
+
+  (* Inserts at point, advances the mark *)
+  let insert_msg (level, msg) =
+    let tags = match level with
+      | Feedback.Error   -> [Tags.Message.error]
+      | Feedback.Warning -> [Tags.Message.warning]
+      | _ -> []
+    in
+    let mark = `MARK mark in
+    let width = Ideutils.textview_width view in
+    Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp width msg);
+    buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"
+  in
+
+  let mv = object (self)
     inherit GObj.widget box#as_widget
 
+    (* List of displayed messages *)
+    val mutable last_width = -1
+    val mutable msgs = []
+
     val push = new GUtil.signal ()
 
     method connect =
       new message_view_signals_impl box#as_widget push
 
+    method refresh force =
+      (* We need to block updates here due to the following race:
+         insertion of messages may create a vertical scrollbar, this
+         will trigger a width change, calling refresh again and
+         going into an infinite loop. *)
+      let width = Ideutils.textview_width view  in
+      (* Could still this method race if the scrollbar changes the
+         textview_width ?? *)
+      let needed = force || last_width <> width in
+      if needed then begin
+        last_width <- width;
+        buffer#set_text "";
+        buffer#move_mark (`MARK mark) ~where:buffer#start_iter;
+        List.(iter insert_msg (rev msgs))
+      end
+
     method clear =
-      buffer#set_text "";
-      buffer#move_mark (`MARK mark) ~where:buffer#start_iter
+      msgs <- []; self#refresh true
 
     method push level msg =
-      let tags = match level with
-      | Feedback.Error -> [Tags.Message.error]
-      | Feedback.Warning -> [Tags.Message.warning]
-      | _ -> []
-      in
-      let rec non_empty = function
-      | Xml_datatype.PCData "" -> false
-      | Xml_datatype.PCData _ -> true
-      | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
-      in
-      if non_empty (Richpp.repr msg) then begin
-        let mark = `MARK mark in
-        Ideutils.insert_xml ~mark buffer ~tags msg;
-        buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
-        push#call (level, msg)
-      end
+      msgs <- (level, msg) :: msgs;
+      insert_msg (level, msg);
+      push#call (level, msg)
 
     method add msg = self#push Feedback.Notice msg
 
-    method add_string s = self#add (Richpp.richpp_of_string s)
+    method add_string s = self#add (Pp.str s)
 
     method set msg = self#clear; self#add msg
 
     method buffer = text_buffer
 
   end
+  in
+  (* Is there a better way to connect the signal ? *)
+  let w_cb (_ : Gtk.rectangle) = mv#refresh false in
+  ignore (view#misc#connect#size_allocate ~callback:w_cb);
+  mv