Fix #9812: CoqIDE on gtk3 has wrong defaults for selection BG.

Unfortunately, the only sane fix I was able to hack was to deactivate
the possibility to change the background colour altogether. Trying to
do otherwise is a real Pandora's box which is ultimately triggered by
the lack of lablgtk3 bindings for the GtkStyleContext class.

I tried a lot of alternative approaches, to no avail. This includes
catching the selection signal, reimplementing selection by hand in
GtkTextView, and even reading the internal details of the GTK
implementation turned not that helpful.

For the time being (8.10 beta) I think we do not have much choice.

7 files changed, 27 insertions, 21 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index e04001974e..47cd4c58b6 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -410,8 +410,8 @@ let vertical_tabs =
 let opposite_tabs =
   new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool)
 
-let background_color =
-  new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
+(* let background_color = *)
+(*   new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) *)
 
 let attach_tag (pref : string preference) (tag : GText.tag) f =
   tag#set_property (f pref#get);
@@ -737,7 +737,7 @@ let configure ?(apply=(fun () -> ())) parent =
       ()
     in
     let () = Util.List.iteri iter [
-      ("Background color", background_color);
+(*       ("Background color", background_color); *)
       ("Background color of processed text", processed_color);
       ("Background color of text being processed", processing_color);
       ("Background color of incompletely processed Qed", incompletely_processed_color);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index d2f1b5ba29..785c191b46 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -88,7 +88,7 @@ val reset_on_tab_switch : bool preference
 val line_ending : line_ending preference
 val vertical_tabs : bool preference
 val opposite_tabs : bool preference
-val background_color : string preference
+(* val background_color : string preference *)
 val processing_color : string preference
 val processed_color : string preference
 val error_color : string preference
diff --git a/ide/session.ml b/ide/session.ml
index fd21515ca5..90412f53f0 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -257,9 +257,10 @@ 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 clr = data#misc#modify_bg [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed ~callback:refresh in
-  let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in
+(* FIXME: handle this using CSS *)
+(*   let refresh clr = data#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(*   let _ = background_color#connect#changed ~callback:refresh in *)
+(*   let _ = data#misc#connect#realize ~callback:(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) ->
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index be400a5f2d..2cadd7ffbf 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -100,9 +100,10 @@ object(self)
     router#register_route route_id result;
     r_bin#add_with_viewport (result :> GObj.widget);
     views <- (frame#coerce, result, combo#entry) :: views;
-    let cb clr = result#misc#modify_bg [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed ~callback:cb in
-    let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
+(* FIXME: handle this using CSS *)
+(*     let cb clr = result#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(*     let _ = background_color#connect#changed ~callback:cb in *)
+(*     let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in *)
     let cb ft = result#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font result cb;
     result#misc#set_can_focus true; (* false causes problems for selection *)
@@ -171,8 +172,9 @@ object(self)
     self#new_page_maker;
     self#new_query_aux ~grab_now:false ();
     frame#misc#hide ();
-    let _ = background_color#connect#changed ~callback:self#refresh_color in
-    self#refresh_color background_color#get;
+(* FIXME: handle this using CSS *)
+(*     let _ = background_color#connect#changed ~callback: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_MessageView.ml b/ide/wg_MessageView.ml
index 7943b099fc..53e004c4e3 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -59,9 +59,10 @@ let message_view () : message_view =
   let _ = buffer#add_selection_clipboard default_clipboard in
   let () = view#set_left_margin 2 in
   view#misc#show ();
-  let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed ~callback:cb in
-  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
+(* FIXME: handle this using CSS *)
+(*   let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(*   let _ = background_color#connect#changed ~callback:cb in *)
+(*   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in *)
   let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
   stick text_font view cb;
 
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 596df227b7..7bf73b5ebe 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -204,9 +204,10 @@ 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_bg [`NORMAL, `NAME clr] in
-  let _ = background_color#connect#changed ~callback:cb in
-  let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
+(* FIXME: handle this using CSS *)
+(*   let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(*   let _ = background_color#connect#changed ~callback:cb in *)
+(*   let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in *)
   let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
   stick text_font view cb;
 
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 8802eb0f1c..c1ed9b7506 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -506,9 +506,10 @@ object (self)
     in
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
     (* Plug on preferences *)
-    let cb clr = self#misc#modify_bg [`NORMAL, `NAME clr] in
-    let _ = background_color#connect#changed ~callback:cb in
-    let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
+(* FIXME: handle this using CSS *)
+(*     let cb clr = self#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(*     let _ = background_color#connect#changed ~callback:cb in *)
+(*     let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in *)
 
     let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in
     stick dynamic_word_wrap self cb;