Imported Upstream version 8.5~beta3+dfsg

1 files changed, 28 insertions, 5 deletions

diff --git a/ide/preferences.ml b/ide/preferences.ml
index c59642d3..90862d06 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -190,7 +190,7 @@ let current = {
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
 
-    modifier_for_navigation = "<Control><Alt>";
+    modifier_for_navigation = "<Control>";
     modifier_for_templates = "<Control><Shift>";
     modifier_for_tactics = "<Control><Alt>";
     modifier_for_display = "<Alt><Shift>";
@@ -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)