Fixed color refresh of command pane

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15218 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 37 insertions, 17 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 939238d3a3..a34e5ebeb3 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -13,6 +13,7 @@ class command_window coqtop current =
 		 ~position:`CENTER
 		 ~title:"CoqIde queries" ~show:false ()
   in *)
+  let views = ref [] in
   let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in
   let _ = frame#misc#hide () in
   let _ = GtkData.AccelGroup.create () in
@@ -49,12 +50,17 @@ class command_window coqtop current =
       ()
   in
 
+  let remove_cb () =
+    let index = notebook#current_page in
+    let () = notebook#remove_page index in
+    views := Minilib.list_filter_i (fun i x -> i <> index) !views
+  in
   let _ =
     toolbar#insert_button
       ~tooltip:"Delete Page"
       ~text:"Delete Page"
       ~icon:(Ideutils.stock_to_widget `DELETE)
-      ~callback:(fun () -> notebook#remove_page notebook#current_page)
+      ~callback:remove_cb
       ()
   in
 object(self)
@@ -63,14 +69,14 @@ object(self)
 
   val new_page_menu = new_page_menu
   val notebook = notebook
+
   method frame = frame
   method new_command ?command ?term () =
-    let appendp x = ignore (notebook#append_page x) in
     let frame = GBin.frame
 		  ~shadow_type:`ETCHED_OUT
-		  ~packing:appendp
 		  ()
     in
+    let _ = notebook#append_page frame#coerce in
     notebook#goto_page (notebook#page_num frame#coerce);
     let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
     let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
@@ -91,7 +97,10 @@ object(self)
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
     let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
     let result = GText.view ~packing:r_bin#add () in
+    let () = views := !views @ [result] in
     result#misc#modify_font !current.Preferences.text_font;
+    let clr = Tags.color_of_string !current.Preferences.background_color in
+    result#misc#modify_base [`NORMAL, `COLOR clr];
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
     let callback () =
@@ -134,6 +143,15 @@ object(self)
     ignore (combo#entry#connect#activate ~callback);
     self#frame#misc#show ()
 
+  method refresh_font () =
+    let iter view = view#misc#modify_font !current.Preferences.text_font in
+    List.iter iter !views
+
+  method refresh_color () =
+    let clr = Tags.color_of_string !current.Preferences.background_color in
+    let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in
+    List.iter iter !views
+
   initializer
     ignore (new_page_menu#connect#clicked ~callback:self#new_command);
    (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index 8c7319aa3d..c34b6cf67a 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -11,4 +11,6 @@ class command_window :
   object
     method new_command : ?command:string -> ?term:string -> unit -> unit
     method frame : GBin.frame
+    method refresh_font : unit -> unit
+    method refresh_color : unit -> unit
   end
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 358302d3c4..a299ffda00 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2804,24 +2804,24 @@ let main files =
   refresh_font_hook :=
     (fun () ->
       let fd = !current.text_font in
-      List.iter
-	(fun {script=view; proof_view=prf_v; message_view=msg_v} ->
-          view#misc#modify_font fd;
-          prf_v#misc#modify_font fd;
-          msg_v#misc#modify_font fd
-        )
-	session_notebook#pages;
+      let iter_page p =
+        p.script#misc#modify_font fd;
+        p.proof_view#misc#modify_font fd;
+        p.message_view#misc#modify_font fd;
+        p.command#refresh_font ()
+      in
+      List.iter iter_page session_notebook#pages;
     );
   refresh_background_color_hook :=
     (fun () ->
       let clr = Tags.color_of_string !current.background_color in
-      List.iter
-        (fun {script=view; proof_view=prf_v; message_view=msg_v} ->
-          view#misc#modify_base [`NORMAL, `COLOR clr];
-          prf_v#misc#modify_base [`NORMAL, `COLOR clr];
-          msg_v#misc#modify_base [`NORMAL, `COLOR clr]
-        )
-        session_notebook#pages;
+      let iter_page p =
+        p.script#misc#modify_base [`NORMAL, `COLOR clr];
+        p.proof_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.message_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.command#refresh_color ()
+      in
+      List.iter iter_page session_notebook#pages;
     );
   resize_window_hook := (fun () ->
     w#resize