diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-07 14:39:18 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-12 16:46:25 +0200 |
commit | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (patch) | |
tree | ae4c146eef03dbb4ebae6f7a28579e3f42878fe7 /ide | |
parent | 238725dd24d43574690b0111761b705753d3bee2 (diff) |
Fixing bug #2498: Coqide navigation preferences delayed effect.
Diffstat (limited to 'ide')
-rw-r--r-- | ide/preferences.ml | 31 |
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) |