aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-12 18:54:10 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-12 19:27:59 +0100
commite9b239881bc32dd15ac53b9463708030c95a9e0c (patch)
tree812a66f6d6343c89892703f0522467939779c31a /ide
parentde8888e28ad793511ba2e2969516325b0be44330 (diff)
Focussing on message view in CoqIDE when a message is pushed.
Also fixes bug #4030.
Diffstat (limited to 'ide')
-rw-r--r--ide/session.ml16
-rw-r--r--ide/wg_MessageView.ml24
-rw-r--r--ide/wg_MessageView.mli8
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