Using the new preference mechanism for colors in CoqIDE.

A lot of legacy code has been removed in the process in favour of
signal-based interactions.

14 files changed, 87 insertions, 177 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 7f44ec2aa..b178ba4ae 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -160,12 +160,11 @@ object
 end
 
 let flags_to_color f =
-  let of_col c = `NAME (Tags.string_of_color c) in
   if List.mem `PROCESSING f then `NAME "blue"
   else if List.mem `ERROR f then `NAME "red"
   else if List.mem `UNSAFE f then `NAME "orange"
   else if List.mem `INCOMPLETE f then `NAME "gray"
-  else of_col (Tags.get_processed_color ())
+  else `NAME Preferences.processed_color#get
 
 module Doc = Document
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e8bdf5e0e..46d99913e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -828,8 +828,6 @@ let refresh_editor_prefs () =
     else 0
   in
   let fd = prefs.text_font in
-  let clr = Tags.color_of_string background_color#get
-  in
   let iter_session sn =
     (* Editor settings *)
     sn.script#set_wrap_mode wrap_mode;
@@ -854,18 +852,6 @@ let refresh_editor_prefs () =
     sn.messages#modify_font fd;
     sn.command#refresh_font ();
 
-    (* Colors *)
-    Tags.set_processing_color (Tags.color_of_string processing_color#get);
-    Tags.set_processed_color (Tags.color_of_string processed_color#get);
-    Tags.set_error_color (Tags.color_of_string error_color#get);
-    Tags.set_error_fg_color (Tags.color_of_string error_fg_color#get);
-    sn.script#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.messages#refresh_color ();
-    sn.command#refresh_color ();
-    sn.errpage#refresh_color ();
-    sn.jobpage#refresh_color ();
-
   in
   List.iter iter_session notebook#pages
 
@@ -1315,13 +1301,12 @@ let build_ui () =
   Tags.Script.incomplete#set_property
     (`BACKGROUND_STIPPLE
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
-  Tags.Script.incomplete#set_property
-    (`BACKGROUND_GDK (Tags.get_processed_color ())); 
 
   (* Showtime ! *)
   w#show ()
 
 
+
 (** {2 Coqide main function } *)
 
 let make_file_buffer f =
diff --git a/ide/preferences.ml b/ide/preferences.ml
index ceae6d1be..74ca6ca83 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -57,6 +57,8 @@ object (self)
   method connect = new preference_signals ~changed
   method get = data
   method set (n : 'a) = data <- n; changed#call n
+  method reset () = self#set default
+  method default = default
 end
 
 (** Useful marshallers *)
@@ -269,19 +271,35 @@ let opposite_tabs =
   new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool)
 
 let background_color =
-  new preference ~name:["background_color"] ~init:Tags.default_color ~repr:Repr.(string)
+  new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
+
+let attach_bg (pref : string preference) (tag : GText.tag) =
+  pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))
+
+let attach_fg (pref : string preference) (tag : GText.tag) =
+  pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))
 
 let processing_color =
-  new preference ~name:["processing_color"] ~init:Tags.default_processing_color ~repr:Repr.(string)
+  new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
+
+let _ = attach_bg processing_color Tags.Script.to_process
+let _ = attach_bg processing_color Tags.Script.incomplete
 
 let processed_color =
-  new preference ~name:["processed_color"] ~init:Tags.default_processed_color ~repr:Repr.(string)
+  new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string)
+
+let _ = attach_bg processed_color Tags.Script.processed
+let _ = attach_bg processed_color Tags.Proof.highlight
 
 let error_color =
-  new preference ~name:["error_color"] ~init:Tags.default_error_color ~repr:Repr.(string)
+  new preference ~name:["error_color"] ~init:"#FFCCCC" ~repr:Repr.(string)
+
+let _ = attach_bg error_color Tags.Script.error_bg
 
 let error_fg_color =
-  new preference ~name:["error_fg_color"] ~init:Tags.default_error_fg_color ~repr:Repr.(string)
+  new preference ~name:["error_fg_color"] ~init:"red" ~repr:Repr.(string)
+
+let _ = attach_fg error_fg_color Tags.Script.error
 
 let dynamic_word_wrap =
   new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool)
@@ -470,75 +488,38 @@ 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:1) ()
-    in
-    let processing_label = GMisc.label
-      ~text:"Background color of text being processed"
-      ~packing:(table#attach ~expand:`X ~left:0 ~top:2) ()
-    in
-    let error_label = GMisc.label
-      ~text:"Background color of errors"
-      ~packing:(table#attach ~expand:`X ~left:0 ~top:3) ()
-    in
-    let error_fg_label = GMisc.label
-      ~text:"Foreground color of errors"
-      ~packing:(table#attach ~expand:`X ~left:0 ~top:4) ()
-    in
-    let () = background_label#set_xalign 0. in
-    let () = processed_label#set_xalign 0. in
-    let () = processing_label#set_xalign 0. in
-    let () = error_label#set_xalign 0. in
-    let () = error_fg_label#set_xalign 0. in
-    let background_button = GButton.color_button
-      ~color:(Tags.color_of_string (background_color#get))
-      ~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:1) ()
-    in
-    let processing_button = GButton.color_button
-      ~color:(Tags.get_processing_color ())
-      ~packing:(table#attach ~left:1 ~top:2) ()
-    in
-    let error_button = GButton.color_button
-      ~color:(Tags.get_error_color ())
-      ~packing:(table#attach ~left:1 ~top:3) ()
-    in
-    let error_fg_button = GButton.color_button
-      ~color:(Tags.get_error_fg_color ())
-      ~packing:(table#attach ~left:1 ~top:4) ()
-    in
     let reset_button = GButton.button
       ~label:"Reset"
       ~packing:box#pack ()
     in
-    let reset_cb () =
-      background_button#set_color Tags.(color_of_string default_color);
-      processing_button#set_color Tags.(color_of_string default_processing_color);
-      processed_button#set_color Tags.(color_of_string default_processed_color);
-      error_button#set_color Tags.(color_of_string default_error_color);
+    let iter i (text, pref) =
+      let label = GMisc.label
+        ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) ()
+      in
+      let () = label#set_xalign 0. in
+      let button = GButton.color_button
+        ~color:(Tags.color_of_string pref#get)
+        ~packing:(table#attach ~left:1 ~top:i) ()
+      in
+      let _ = button#connect#color_set begin fun () ->
+        pref#set (Tags.string_of_color button#color)
+      end in
+      let reset _ =
+        pref#reset ();
+        button#set_color Tags.(color_of_string pref#get)
+      in
+      let _ = reset_button#connect#clicked ~callback:reset in
+      ()
     in
-    let _ = reset_button#connect#clicked ~callback:reset_cb in
+    let () = Util.List.iteri iter [
+      ("Background color", background_color);
+      ("Background color of processed text", processed_color);
+      ("Background color of text being processed", processing_color);
+      ("Background color of errors", error_color);
+      ("Foreground color of errors", error_fg_color);
+    ] in
     let label = "Color configuration" in
-    let callback () =
-      background_color#set (Tags.string_of_color background_button#color);
-      processing_color#set (Tags.string_of_color processing_button#color);
-      processed_color#set (Tags.string_of_color processed_button#color);
-      error_color#set (Tags.string_of_color error_button#color);
-      error_fg_color#set (Tags.string_of_color error_fg_button#color);
-      !refresh_editor_hook ();
-      Tags.set_processing_color processing_button#color;
-      Tags.set_processed_color processed_button#color;
-      Tags.set_error_color error_button#color;
-      Tags.set_error_fg_color error_fg_button#color
-    in
+    let callback () = () in
     custom ~label box callback true
   in
 
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1da8b3157..48c2a6410 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -29,6 +29,8 @@ object
   method connect : 'a preference_signals
   method get : 'a
   method set : 'a -> unit
+  method reset : unit -> unit
+  method default : 'a
 end
 
 val cmd_coqtop : string option preference
diff --git a/ide/session.ml b/ide/session.ml
index 0b26c1f65..ceeb0abca 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -18,7 +18,6 @@ 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 =
@@ -254,10 +253,9 @@ let make_table_widget ?sort cd cb =
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
-  let refresh () =
-    let clr = Tags.color_of_string background_color#get in
-    data#misc#modify_base [`NORMAL, `COLOR clr]
-  in
+  let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
+  let _ = background_color#connect#changed refresh in
+  let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -285,10 +283,10 @@ let make_table_widget ?sort cd cb =
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
   let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in
-  frame, (fun f -> f columns store), refresh
+  frame, (fun f -> f columns store)
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
-  let table, access, refresh =
+  let table, access =
     make_table_widget ~sort:(0, `ASCENDING)
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
@@ -320,11 +318,10 @@ 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, refresh =
+  let table, access =
     make_table_widget ~sort:(0, `ASCENDING)
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
@@ -360,7 +357,6 @@ 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 52e557218..3a6b45858 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,7 +14,6 @@ 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/tags.ml b/ide/tags.ml
index c9b57af4c..09b562530 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,28 +13,15 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
-(* These work fine for colorblind people too *)
-let default_processed_color = "light green"
-let default_processing_color = "light blue"
-let default_error_color = "#FFCCCC"
-let default_error_fg_color = "red"
-let default_color = "cornsilk"
-
-let processed_color = ref default_processed_color
-let processing_color = ref default_processing_color
-let error_color = ref default_error_color
-let error_fg_color = ref default_error_fg_color
-
 module Script =
 struct
   let table = GText.tag_table ()
   let comment = make_tag table ~name:"comment" []
-  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color]
-  let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color]
+  let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
+  let error_bg = make_tag table ~name:"error_bg" []
+  let to_process = make_tag table ~name:"to_process" []
+  let processed = make_tag table ~name:"processed" []
   let incomplete = make_tag table ~name:"incomplete" [
-          `BACKGROUND !processing_color;
           `BACKGROUND_STIPPLE_SET true;
   ]
   let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
@@ -56,7 +43,7 @@ end
 module Proof =
 struct
   let table = GText.tag_table ()
-  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
+  let highlight = make_tag table ~name:"highlight" []
   let hypothesis = make_tag table ~name:"hypothesis" []
   let goal = make_tag table ~name:"goal" []
 end
@@ -77,34 +64,3 @@ let string_of_color clr =
 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.incomplete#set_property (`BACKGROUND s);
-  Script.to_process#set_property (`BACKGROUND s)
-
-let get_error_color () = color_of_string !error_color
-
-let set_error_color clr =
-  let s = string_of_color clr in
-  error_color := s;
-  Script.error_bg#set_property (`BACKGROUND s)
-
-let get_error_fg_color () = color_of_string !error_fg_color
-
-let set_error_fg_color clr =
-  let s = string_of_color clr in
-  error_fg_color := s;
-  Script.error#set_property (`FOREGROUND s)
-
diff --git a/ide/tags.mli b/ide/tags.mli
index 14cfd0dbf..6418d1b2e 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -41,22 +41,3 @@ 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
-
-val get_error_color : unit -> Gdk.color
-val set_error_color : Gdk.color -> unit
-
-val get_error_fg_color : unit -> Gdk.color
-val set_error_fg_color : Gdk.color -> unit
-
-val default_processed_color : string
-val default_processing_color : string
-val default_error_color : string
-val default_error_fg_color : string
-val default_color : string
-
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
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index 91a8f26ca..c559ebef3 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -11,7 +11,6 @@ class command_window : string -> Coq.coqtop ->
     method new_query : ?command:string -> ?term:string -> unit -> unit
     method pack_in : (GObj.widget -> unit) -> unit
     method refresh_font : unit -> unit
-    method refresh_color : unit -> unit
     method show : unit
     method hide : unit
     method visible : bool
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 3fff01945..7b7f0fab1 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Preferences
+
 class type message_view_signals =
 object
   inherit GObj.misc_signals
@@ -33,7 +35,6 @@ 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 =
@@ -53,6 +54,10 @@ let message_view () : message_view =
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
   let () = view#set_left_margin 2 in
+  view#misc#show ();
+  let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+  let _ = background_color#connect#changed cb in
+  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
   object (self)
     inherit GObj.widget box#as_widget
 
@@ -84,9 +89,4 @@ 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 background_color#get in
-      view#misc#modify_base [`NORMAL, `COLOR clr]
-
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 23c94f404..4dcd7306b 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -25,7 +25,6 @@ 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
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 69d460b01..e3a741394 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Preferences
 
 class type proof_view =
   object
@@ -193,6 +194,9 @@ let proof_view () =
   let () = Gtk_parsing.fix_double_click view in
   let default_clipboard = GData.clipboard Gdk.Atom.primary in
   let _ = buffer#add_selection_clipboard default_clipboard in
+  let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
+  let _ = background_color#connect#changed cb in
+  let _ = view#misc#connect#realize (fun () -> cb background_color#get) in
   object
     inherit GObj.widget view#as_widget
     val mutable goals = None
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 8298d9954..3b3d9db4b 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Preferences
+
 type insert_action = {
   ins_val : string;
   ins_off : int;
@@ -456,6 +458,10 @@ object (self)
       if not proceed then GtkSignal.stop_emit ()
     in
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
+    (** Plug on preferences *)
+    let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
+    let _ = background_color#connect#changed cb in
+    let _ = self#misc#connect#realize (fun () -> cb background_color#get) in
     ()
 
 end