aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2017-06-20 12:48:22 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2017-06-20 12:48:22 +0200
commit43e141c5bcc0a9745f89061c94fe953c15e8d5c0 (patch)
tree10a0b52f37bd6b3b290bf4093a6caa6e4c4aade5 /ide
parent409f73f6e69b7c62ae3bdf1686fa3cc9ccc06e9f (diff)
Default colors for CoqIDE are actually applied.
This fixes bug #5380 in particular. More generally, tags were not updated to the correct default value if the corresponding line in the configuration file was missing.
Diffstat (limited to 'ide')
-rw-r--r--ide/preferences.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8559533de..56bf91a09 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -407,11 +407,15 @@ let opposite_tabs =
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);
+ pref#connect#changed (fun c -> tag#set_property (f c))
+
let attach_bg (pref : string preference) (tag : GText.tag) =
- pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c))
+ attach_tag pref tag (fun c -> `BACKGROUND c)
let attach_fg (pref : string preference) (tag : GText.tag) =
- pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c))
+ attach_tag pref tag (fun c -> `FOREGROUND c)
let processing_color =
new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)