aboutsummaryrefslogtreecommitdiff
path: root/ide/wg_Command.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-04-08 16:03:05 +0200
committerPierre-Marie Pédrot2019-04-08 16:07:11 +0200
commitdf91339e6b1da481b5cbb4db48a205a7a1bc906b (patch)
tree70eeee7a71ec0f66645e3335e8a34092988202e5 /ide/wg_Command.ml
parent81df7850d40273814fcf78cf6df9057f19fa9a8e (diff)
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.
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r--ide/wg_Command.ml12
1 files changed, 7 insertions, 5 deletions
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