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/coqide.ml | |
| parent | 1e5a7ded7b5ca5b2cca548f9a80ff8fd805e6ba1 (diff) | |
Fixing bug #4023.
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 5 |
1 files changed, 3 insertions, 2 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")); |