aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-06-07 14:39:18 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-09-12 16:46:25 +0200
commit490160d25d3caac1d2ea5beebbbebc959b1b3832 (patch)
treeae4c146eef03dbb4ebae6f7a28579e3f42878fe7 /ide
parent238725dd24d43574690b0111761b705753d3bee2 (diff)
Fixing bug #2498: Coqide navigation preferences delayed effect.
Diffstat (limited to 'ide')
-rw-r--r--ide/preferences.ml31
1 files changed, 27 insertions, 4 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c59642d3a..1bd9f587c 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -711,38 +711,61 @@ let configure ?(apply=(fun () -> ())) () =
~f:(fun s -> current.project_file_name <- s)
current.project_file_name
in
+ let update_modifiers prefix mds =
+ let change ~path ~key ~modi ~changed =
+ if CString.is_sub prefix path 0 then
+ ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path)
+ in
+ GtkData.AccelMap.foreach change
+ in
let help_string =
"restart to apply"
in
let the_valid_mod = str_to_mod_list current.modifiers_valid in
let modifier_for_tactics =
+ let cb l =
+ current.modifier_for_tactics <- mod_list_to_str l;
+ update_modifiers "<Actions>/Tactics/" l
+ in
modifiers
~allow:the_valid_mod
- ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
+ ~f:cb
~help:help_string
"Modifiers for Tactics Menu"
(str_to_mod_list current.modifier_for_tactics)
in
let modifier_for_templates =
+ let cb l =
+ current.modifier_for_templates <- mod_list_to_str l;
+ update_modifiers "<Actions>/Templates/" l
+ in
modifiers
~allow:the_valid_mod
- ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
+ ~f:cb
~help:help_string
"Modifiers for Templates Menu"
(str_to_mod_list current.modifier_for_templates)
in
let modifier_for_navigation =
+ let cb l =
+ current.modifier_for_navigation <- mod_list_to_str l;
+ update_modifiers "<Actions>/Navigation/" l
+ in
modifiers
~allow:the_valid_mod
- ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
+ ~f:cb
~help:help_string
"Modifiers for Navigation Menu"
(str_to_mod_list current.modifier_for_navigation)
in
let modifier_for_display =
+ let cb l =
+ current.modifier_for_display <- mod_list_to_str l;
+ update_modifiers "<Actions>/View/" l
+ in
modifiers
~allow:the_valid_mod
- ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
+ ~f:cb
~help:help_string
"Modifiers for View Menu"
(str_to_mod_list current.modifier_for_display)