Added a background color configuration option in CoqIDE.

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

5 files changed, 90 insertions, 15 deletions

diff --git a/ide/coqide-gtk2rc b/ide/coqide-gtk2rc
index 621d4e847..9da99551b 100644
--- a/ide/coqide-gtk2rc
+++ b/ide/coqide-gtk2rc
@@ -23,16 +23,6 @@ binding "text" {
 class "GtkTextView" binding "text"
 
 
-style "views" {
-base[NORMAL] = "CornSilk"
-# bg_pixmap[NORMAL] = "background.jpg"
-}
-class "GtkTextView" style "views"
-
-widget "*.*.*.*.*.ScriptWindow" style "views"
-widget "*.*.*.*.GoalWindow" style "views"
-widget "*.*.*.*.MessageWindow" style "views"
-
 gtk-font-name = "Sans 12"
 
 style "location" {
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c31fb76f3..b884c5306 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1525,9 +1525,15 @@ let create_session file =
   script#buffer#place_cursor ~where:(script#buffer#start_iter);
   proof#misc#set_can_focus true;
   message#misc#set_can_focus true;
+  (* setting fonts *)
   script#misc#modify_font !current.text_font;
   proof#misc#modify_font !current.text_font;
   message#misc#modify_font !current.text_font;
+  (* setting colors *)
+  script#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  proof#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  message#misc#modify_base [`NORMAL, `NAME !current.background_color];
+
   { tab_label=basename;
     filename=begin match file with None -> "" |Some f -> f end;
     script=script;
@@ -2804,6 +2810,16 @@ let main files =
         )
 	session_notebook#pages;
     );
+  change_background_color :=
+    (fun clr ->
+      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 about_full_string =
     "\nCoq is developed by the Coq Development Team\
      \n(INRIA - CNRS - LIX - LRI - PPS)\
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 80caefa5f..828294c33 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -93,6 +93,7 @@ type pref =
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
 
+      mutable background_color : string;
       mutable processing_color : string;
       mutable processed_color : string;
 
@@ -158,6 +159,7 @@ let (current:pref ref) =
     vertical_tabs = false;
     opposite_tabs = false;
 
+    background_color = "cornsilk";
     processed_color = "light green";
     processing_color = "light blue";
 
@@ -166,6 +168,8 @@ let (current:pref ref) =
 
 let change_font = ref (fun f -> ())
 
+let change_background_color = ref (fun clr -> ())
+
 let show_toolbar = ref (fun x -> ())
 
 let auto_complete = ref (fun x -> ())
@@ -228,6 +232,7 @@ let save_pref () =
     add "lax_syntax" [string_of_bool p.lax_syntax] ++
     add "vertical_tabs" [string_of_bool p.vertical_tabs] ++
     add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
+    add "background_color" [p.background_color] ++
     add "processing_color" [p.processing_color] ++
     add "processed_color" [p.processed_color] ++
     Config_lexer.print_file pref_file
@@ -303,6 +308,7 @@ let load_pref () =
     set_bool "lax_syntax" (fun v -> np.lax_syntax <- v);
     set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v);
     set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
+    set_hd "background_color" (fun v -> np.background_color <- v);
     set_hd "processing_color" (fun v -> np.processing_color <- v);
     set_hd "processed_color" (fun v -> np.processed_color <- v);
     current := np
@@ -362,28 +368,39 @@ let configure ?(apply=(fun () -> ())) () =
       ~border_width:2
       ~packing:(box#pack ~expand:true) ()
     in
+    let background_label = GMisc.label
+      ~text:"Background color"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:0) ()
+    in
     let processed_label = GMisc.label
       ~text:"Background color of processed text"
-      ~packing:(table#attach ~expand:`X ~left:0 ~top:0) ()
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:1) ()
     in
     let processing_label = GMisc.label
       ~text:"Background color of text being processed"
-      ~packing:(table#attach ~expand:`X ~left:0 ~top:1) ()
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:2) ()
     in
+    let () = background_label#set_xalign 0. in
     let () = processed_label#set_xalign 0. in
     let () = processing_label#set_xalign 0. in
+    let background_button = GButton.color_button
+      ~color:(Tags.color_of_string (!current.background_color))
+      ~packing:(table#attach ~left:1 ~top:0) ()
+    in
     let processed_button = GButton.color_button
       ~color:(Tags.get_processed_color ())
-      ~packing:(table#attach ~left:1 ~top:0) ()
+      ~packing:(table#attach ~left:1 ~top:1) ()
     in
     let processing_button = GButton.color_button
       ~color:(Tags.get_processing_color ())
-      ~packing:(table#attach ~left:1 ~top:1) ()
+      ~packing:(table#attach ~left:1 ~top:2) ()
     in
     let label = "Color configuration" in
     let callback () =
+      !current.background_color <- Tags.string_of_color background_button#color;
       !current.processing_color <- Tags.string_of_color processing_button#color;
       !current.processed_color <- Tags.string_of_color processed_button#color;
+      !change_background_color background_button#color;
       Tags.set_processing_color processing_button#color;
       Tags.set_processed_color processed_button#color
     in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 245514bd9..292e43972 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -61,6 +61,7 @@ type pref =
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
 
+      mutable background_color : string;
       mutable processing_color : string;
       mutable processed_color : string;
     }
@@ -72,7 +73,8 @@ val current : pref ref
 
 val configure : ?apply:(unit -> unit) -> unit -> unit
 
-val change_font : ( Pango.font_description -> unit) ref
+val change_font : (Pango.font_description -> unit) ref
+val change_background_color : (Gdk.color -> unit) ref
 val show_toolbar : (bool -> unit) ref
 val auto_complete : (bool -> unit) ref
 val resize_window : (unit -> unit) ref
diff --git a/ide/tags.mli b/ide/tags.mli
new file mode 100644
index 000000000..53a8c4930
--- /dev/null
+++ b/ide/tags.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Script :
+sig
+  val table : GText.tag_table
+  val kwd : GText.tag
+  val qed : GText.tag
+  val decl : GText.tag
+  val proof_decl : GText.tag
+  val comment : GText.tag
+  val reserved : GText.tag
+  val error : GText.tag
+  val to_process : GText.tag
+  val processed : GText.tag
+  val unjustified : GText.tag
+  val found : GText.tag
+  val hidden : GText.tag
+  val folded : GText.tag
+  val paren : GText.tag
+  val sentence : GText.tag
+end
+
+module Proof :
+sig
+  val table : GText.tag_table
+  val highlight : GText.tag
+  val hypothesis : GText.tag
+  val goal : GText.tag
+end
+
+module Message :
+sig
+  val table : GText.tag_table
+  val error : GText.tag
+end
+
+val string_of_color : Gdk.color -> string
+val color_of_string : string -> Gdk.color
+
+val get_processed_color : unit -> Gdk.color
+val set_processed_color : Gdk.color -> unit
+
+val get_processing_color : unit -> Gdk.color
+val set_processing_color : Gdk.color -> unit