diff options
Diffstat (limited to 'ide/wg_MessageView.ml')
| -rw-r--r-- | ide/wg_MessageView.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index b32674084d..211db537ed 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -33,6 +33,7 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit + method refresh_color : unit -> unit end let message_view () : message_view = @@ -83,4 +84,9 @@ let message_view () : message_view = method modify_font fd = view#misc#modify_font fd + method refresh_color () = + let open Preferences in + let clr = Tags.color_of_string current.background_color in + view#misc#modify_base [`NORMAL, `COLOR clr] + end |