diff options
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r-- | ide/wg_Command.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index bf25ddfa1..bfd37ea0e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -86,8 +86,9 @@ object(self) let result = GText.view ~packing:r_bin#add () in views <- (frame#coerce, result, combo#entry) :: views; result#misc#modify_font current.text_font; - let clr = Tags.color_of_string background_color#get in - result#misc#modify_base [`NORMAL, `COLOR clr]; + let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed cb in + let _ = result#misc#connect#realize (fun () -> cb background_color#get) in result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; let callback () = @@ -149,8 +150,8 @@ object(self) let iter (_,view,_) = view#misc#modify_font current.text_font in List.iter iter views - method refresh_color () = - let clr = Tags.color_of_string background_color#get in + method private refresh_color clr = + let clr = Tags.color_of_string clr in let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in List.iter iter views @@ -158,6 +159,8 @@ object(self) self#new_page_maker; self#new_query_aux ~grab_now:false (); frame#misc#hide (); + let _ = background_color#connect#changed self#refresh_color in + self#refresh_color background_color#get; ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) else false |