diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 16:09:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 16:09:01 +0100 |
| commit | cf4645acc78a8463fa533756efd9a8d9855d727d (patch) | |
| tree | 708baee8ba966b2d93e99bb463b345ecc5661e10 /ide | |
| parent | 1e5a7ded7b5ca5b2cca548f9a80ff8fd805e6ba1 (diff) | |
Fixing bug #4023.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 5 | ||||
| -rw-r--r-- | ide/preferences.ml | 5 |
2 files changed, 4 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index fa64defab..78fcbaf8c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -838,6 +838,9 @@ let refresh_editor_prefs () = sn.command#refresh_font (); (* Colors *) + Tags.set_processing_color (Tags.color_of_string current.processing_color); + Tags.set_processed_color (Tags.color_of_string current.processed_color); + Tags.set_error_color (Tags.color_of_string current.error_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; @@ -1314,8 +1317,6 @@ let build_ui () = refresh_tabs_hook := refresh_notebook_pos; (* Color configuration *) - Tags.set_processing_color (Tags.color_of_string prefs.processing_color); - Tags.set_processed_color (Tags.color_of_string prefs.processed_color); Tags.Script.incomplete#set_property (`BACKGROUND_STIPPLE (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); diff --git a/ide/preferences.ml b/ide/preferences.ml index c85061325..25712f951 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -503,10 +503,7 @@ let configure ?(apply=(fun () -> ())) () = current.processing_color <- Tags.string_of_color processing_button#color; current.processed_color <- Tags.string_of_color processed_button#color; current.error_color <- Tags.string_of_color error_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 + !refresh_editor_hook () in custom ~label box callback true in |