Merge branch 'v8.5'

1 files changed, 23 insertions, 1 deletions

diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 9acda53fc3..09f1d44535 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -6,9 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+class type message_view_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
+class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
+object
+  val after = false
+  inherit GObj.misc_signals obj
+  inherit GUtil.add_ml_signals obj [pushed#disconnect]
+  method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s)
+end
+
 class type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit
@@ -38,6 +54,11 @@ let message_view () : message_view =
   object (self)
     inherit GObj.widget box#as_widget
 
+    val push = new GUtil.signal ()
+
+    method connect =
+      new message_view_signals_impl box#as_widget push
+
     method clear =
       buffer#set_text ""
 
@@ -49,7 +70,8 @@ let message_view () : message_view =
       in
       if msg <> "" then begin
         buffer#insert ~tags msg;
-        buffer#insert ~tags "\n"
+        buffer#insert ~tags "\n";
+        push#call (level, msg)
       end
 
     method add msg = self#push Pp.Notice msg