diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 01:29:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 03:53:40 +0200 |
| commit | 5a90c69f8e4699f205ec3e59cfd49ad9fb9f6f87 (patch) | |
| tree | 9d31cb58d1c6166beec1757668e73ad5d794b0d6 /ide/wg_Command.ml | |
| parent | 2c70dd6a256ed4cac2b74bd0c8719ab37fffcb84 (diff) | |
Turning CoqIDE preferences into new style.
Some old style references remain because all type converters are not
implemented yet.
Diffstat (limited to 'ide/wg_Command.ml')
| -rw-r--r-- | ide/wg_Command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 7dad92ed6..bf25ddfa1 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -86,7 +86,7 @@ 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 current.background_color in + let clr = Tags.color_of_string background_color#get in result#misc#modify_base [`NORMAL, `COLOR clr]; result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; @@ -150,7 +150,7 @@ object(self) List.iter iter views method refresh_color () = - let clr = Tags.color_of_string current.background_color in + let clr = Tags.color_of_string background_color#get in let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in List.iter iter views |