A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.

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

5 files changed, 92 insertions, 5 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 111a8ffc2..c31fb76f3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2183,6 +2183,7 @@ let main files =
 	     true))
   in reset_auto_save_timer (); (* to enable statup preferences timer *)
 (* end Preferences *)
+
   let do_or_activate f () =
     do_if_not_computing "do_or_activate"
       (fun current ->
@@ -2867,6 +2868,12 @@ let main files =
   (*
 
   *)
+(* Begin Color configuration *)
+
+  Tags.set_processing_color (Tags.color_of_string !current.processing_color);
+  Tags.set_processed_color (Tags.color_of_string !current.processed_color);
+
+(* End of color configuration *)
   resize_window := (fun () ->
     w#resize
       ~width:!current.window_width
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 02673098b..abfa1857e 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -92,6 +92,10 @@ type pref =
       mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+
+      mutable processing_color : string;
+      mutable processed_color : string;
+
 }
 
 let use_default_doc_url = "(automatic)"
@@ -153,6 +157,10 @@ let (current:pref ref) =
     lax_syntax = true;
     vertical_tabs = false;
     opposite_tabs = false;
+
+    processing_color = "light green";
+    processed_color = "light blue";
+
   }
 
 
@@ -220,6 +228,8 @@ 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 "processing_color" [p.processing_color] ++
+    add "processed_color" [p.processed_color] ++
     Config_lexer.print_file pref_file
 
 let load_pref () =
@@ -293,6 +303,8 @@ 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 "processing_color" (fun v -> np.processing_color <- v);
+    set_hd "processed_color" (fun v -> np.processed_color <- v);
     current := np
 (*
     Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
@@ -325,7 +337,7 @@ let configure ?(apply=(fun () -> ())) () =
     let w = GMisc.font_selection () in
     w#set_preview_text
       "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
-    box#pack w#coerce;
+    box#pack ~expand:true w#coerce;
     ignore (w#misc#connect#realize
 	      ~callback:(fun () -> w#set_font_name
 			   (Pango.Font.to_string !current.text_font)));
@@ -341,6 +353,43 @@ let configure ?(apply=(fun () -> ())) () =
 	 !change_font !current.text_font)
       true
   in
+
+  let config_color =
+    let box = GPack.hbox () in
+    let table = GPack.table
+      ~row_spacings:5
+      ~col_spacings:5
+      ~border_width:2
+      ~packing:(box#pack ~expand:true) ()
+    in
+    let processed_label = GMisc.label
+      ~text:"Background color of processed text"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:0) ()
+    in
+    let processing_label = GMisc.label
+      ~text:"Background color of text being processed"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:1) ()
+    in
+    let () = processed_label#set_xalign 0. in
+    let () = processing_label#set_xalign 0. in
+    let processed_button = GButton.color_button
+      ~color:(Tags.get_processed_color ())
+      ~packing:(table#attach ~left:1 ~top:0) ()
+    in
+    let processing_button = GButton.color_button
+      ~color:(Tags.get_processing_color ())
+      ~packing:(table#attach ~left:1 ~top:1) ()
+    in
+    let label = "Color configuration" in
+    let callback () =
+      !current.processing_color <- Tags.string_of_color processing_button#color;
+      !current.processed_color <- Tags.string_of_color processed_button#color;
+      Tags.set_processing_color processing_button#color;
+      Tags.set_processed_color processed_button#color
+    in
+    custom ~label box callback true
+  in
+
 (*
   let show_toolbar =
     bool
@@ -591,6 +640,7 @@ let configure ?(apply=(fun () -> ())) () =
   let cmds =
     [Section("Fonts", Some `SELECT_FONT,
 	     [config_font]);
+     Section("Colors", Some `SELECT_COLOR, [config_color]);
      Section("Files", Some `DIRECTORY,
 	     [global_auto_revert;global_auto_revert_delay;
 	      auto_save; auto_save_delay; (* auto_save_name*)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index f55088f11..245514bd9 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -60,6 +60,9 @@ type pref =
       mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+
+      mutable processing_color : string;
+      mutable processed_color : string;
     }
 
 val save_pref : unit -> unit
diff --git a/ide/tags.ml b/ide/tags.ml
index 52ba54dcb..eeace4658 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,6 +13,9 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
+let processed_color = ref "light green"
+let processing_color = ref "light blue"
+
 module Script =
 struct
   let table = GText.tag_table ()
@@ -23,8 +26,8 @@ struct
   let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"]
   let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"]
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]
+  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
+  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false]
   let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false]
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
@@ -35,7 +38,7 @@ end
 module Proof =
 struct
   let table = GText.tag_table ()
-  let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"]
+  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
   let hypothesis = make_tag table ~name:"hypothesis" []
   let goal = make_tag table ~name:"goal" []
 end
@@ -45,3 +48,27 @@ struct
   let error = make_tag table ~name:"error" [`FOREGROUND "red"]
 end
 
+let string_of_color clr =
+  let r = Gdk.Color.red clr in
+  let g = Gdk.Color.green clr in
+  let b = Gdk.Color.blue clr in
+  Printf.sprintf "#%04X%04X%04X" r g b
+
+let color_of_string s =
+  let colormap = Gdk.Color.get_system_colormap () in
+  Gdk.Color.alloc ~colormap (`NAME s)
+
+let get_processed_color () = color_of_string !processed_color
+
+let set_processed_color clr =
+  let s = string_of_color clr in
+  processed_color := s;
+  Script.processed#set_property (`BACKGROUND s);
+  Proof.highlight#set_property (`BACKGROUND s)
+
+let get_processing_color () = color_of_string !processing_color
+
+let set_processing_color clr =
+  let s = string_of_color clr in
+  processing_color := s;
+  Script.to_process#set_property (`BACKGROUND s)
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 9ddc90ef1..c13a0b3cf 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1022,7 +1022,7 @@ class configuration_box (tt : GData.tooltips) conf_struct =
 
   let rec make_tree iter conf_struct =
     (* box is not shown at first *)
-    let box = GPack.vbox ~packing:menu_box#add ~show:false () in
+    let box = GPack.vbox ~packing:(menu_box#pack ~expand:true) ~show:false () in
     let new_iter = match iter with
     | None -> tree#append ()
     | Some parent -> tree#append ~parent ()