aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/preferences.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 08:23:36 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-24 08:26:24 +0200
commit8a031dc29abf1e16b2ee78322a7221b8b5c19a33 (patch)
tree8095b021d3ed73ee9162529a6a3ff4fcbd209a9e /ide/preferences.ml
parentf2f146a997e92f3380d9cd9aa0f7aef80f50dba8 (diff)
Fixing unsetting of CoqIDE tags.
Diffstat (limited to 'ide/preferences.ml')
-rw-r--r--ide/preferences.ml30
1 files changed, 20 insertions, 10 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index dedd62902..313d97086 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -402,24 +402,34 @@ let create_tag name default =
let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in
let set_tag tag =
begin match pref#get.tag_bg_color with
- | None -> ()
- | Some c -> tag#set_property (`BACKGROUND c)
+ | None -> tag#set_property (`BACKGROUND_SET false)
+ | Some c ->
+ tag#set_property (`BACKGROUND_SET true);
+ tag#set_property (`BACKGROUND c)
end;
begin match pref#get.tag_fg_color with
- | None -> ()
- | Some c -> tag#set_property (`FOREGROUND c)
+ | None -> tag#set_property (`FOREGROUND_SET false)
+ | Some c ->
+ tag#set_property (`FOREGROUND_SET true);
+ tag#set_property (`FOREGROUND c)
end;
begin match pref#get.tag_bold with
- | false -> ()
- | true -> tag#set_property (`WEIGHT `BOLD)
+ | false -> tag#set_property (`WEIGHT_SET false)
+ | true ->
+ tag#set_property (`WEIGHT_SET true);
+ tag#set_property (`WEIGHT `BOLD)
end;
begin match pref#get.tag_italic with
- | false -> ()
- | true -> tag#set_property (`STYLE `ITALIC)
+ | false -> tag#set_property (`STYLE_SET false)
+ | true ->
+ tag#set_property (`STYLE_SET true);
+ tag#set_property (`STYLE `ITALIC)
end;
begin match pref#get.tag_underline with
- | false -> ()
- | true -> tag#set_property (`UNDERLINE `SINGLE)
+ | false -> tag#set_property (`UNDERLINE_SET false)
+ | true ->
+ tag#set_property (`UNDERLINE_SET true);
+ tag#set_property (`UNDERLINE `SINGLE)
end;
in
let iter table =