Focussing on message view in CoqIDE when a message is pushed.

Also fixes bug #4030.

3 files changed, 43 insertions, 5 deletions

diff --git a/ide/session.ml b/ide/session.ml
index 293632112..072ae61c6 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -465,7 +465,7 @@ let build_layout (sn:session) =
       message_frame#misc#show ();
       detachable#show);
     detachable#button#misc#hide ();
-    lbl in
+    detachable, lbl in
   let session_tab = GPack.hbox ~homogeneous:false () in
   let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
     ~packing:session_tab#pack () in
@@ -496,9 +496,17 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce);
-  let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
-  ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce);
+  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+  let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
+  let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
+  (** When a message is received, focus on the message pane *)
+  let _ =
+    sn.messages#connect#pushed ~callback:(fun _ _ ->
+      let num = message_frame#page_num detach#coerce in
+      if 0 <= num then message_frame#goto_page num
+    )
+  in
+  (** When an error occurs, paint the error label in red *)
   let txt = label#text in
   let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in
   sn.errpage#on_update ~callback:(fun l ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 9acda53fc..09f1d4453 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
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index cd3f00c97..4dcd7306b 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -6,9 +6,17 @@
 (*         *       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 type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit