diff options
Diffstat (limited to 'ide/wg_MessageView.ml')
| -rw-r--r-- | ide/wg_MessageView.ml | 24 |
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 |