Fixing bug #4073.

5 files changed, 22 insertions, 5 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4564d620e..c977879a7 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -855,8 +855,10 @@ let refresh_editor_prefs () =
     Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color);
     sn.script#misc#modify_base [`NORMAL, `COLOR clr];
     sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.command#refresh_color ()
+    sn.messages#refresh_color ();
+    sn.command#refresh_color ();
+    sn.errpage#refresh_color ();
+    sn.jobpage#refresh_color ();
 
   in
   List.iter iter_session notebook#pages
diff --git a/ide/session.ml b/ide/session.ml
index dc79fa790..e0466b7e3 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -18,6 +18,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
@@ -256,6 +257,10 @@ let make_table_widget cd cb =
       ~rules_hint:true ~headers_visible:false
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
+  let refresh () =
+    let clr = Tags.color_of_string current.background_color in
+    data#misc#modify_base [`NORMAL, `COLOR clr]
+  in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -271,10 +276,10 @@ let make_table_widget cd cb =
   ignore(
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
-  frame, (fun f -> f columns store)
+  frame, (fun f -> f columns store), refresh
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
@@ -305,10 +310,11 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_jobpage coqtop coqops : jobpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
@@ -344,6 +350,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 3a6b45858..52e557218 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index b32674084..211db537e 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
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 4dcd7306b..23c94f404 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -25,6 +25,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
 
 val message_view : unit -> message_view