From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 ide/preferences.ml | 42 +++++++++++++-----------------------------
 1 file changed, 13 insertions(+), 29 deletions(-)

(limited to 'ide/preferences.ml')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 90862d06..f7cc27a5 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -711,61 +711,38 @@ 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:cb
+      ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
       ~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:cb
+      ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
       ~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:cb
+      ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
       ~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:cb
+      ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
       ~help:help_string
       "Modifiers for View Menu"
       (str_to_mod_list current.modifier_for_display)
@@ -777,6 +754,13 @@ let configure ?(apply=(fun () -> ())) () =
       "Allowed modifiers"
       the_valid_mod
   in
+  let modifier_notice =
+    let b = GPack.hbox () in
+    let _lbl =
+      GMisc.label ~markup:"You need to <b>restart CoqIDE</b> after changing these settings"
+        ~packing:b#add () in
+    custom b (fun () -> ()) true
+  in
   let cmd_editor =
     let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
     combo
@@ -878,7 +862,7 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
+	      modifier_for_templates; modifier_for_display; modifier_for_navigation; modifier_notice]);
      Section("Misc", Some `ADD,
 	     misc)]
   in
-- 
cgit v1.2.3