Add an option to configure the modifier for Queries.

3 files changed, 22 insertions, 11 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index d4f47b15e..8b164d234 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -919,7 +919,7 @@ let template_item (text, offset, len, key) =
 (** Create menu items for pairs (query, shortcut key).
     If the shortcut key is not in the range 'a'-'z','A'-'Z', it will be ignored.  *)
 
-let user_queries_items menu_name item_name l modifier =
+let user_queries_items menu_name item_name l =
   let valid_key k = Int.equal (CString.length k) 1 && Util.is_letter k.[0] in
   let mk_item (query, key) =
     let query' =
@@ -929,7 +929,7 @@ let user_queries_items menu_name item_name l modifier =
       else query ^ "."
     in
     let callback = Query.simplequery query' in
-    let accel = if valid_key key then Some (modifier^key) else None in
+    let accel = if valid_key key then Some (modifier_for_queries#get^key) else None in
     item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name
   in
   List.iter mk_item l
@@ -1123,17 +1123,21 @@ let build_ui () =
   ];
   alpha_items templates_menu "Template" Coq_commands.commands;
 
-  let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
+  let qitem s sc =
+    item s ~label:("_"^s)
+      ~accel:(modifier_for_queries#get^sc)
+      ~callback:(Query.query s)
+  in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "Search" (Some "<Ctrl><Shift>K");
-    qitem "Check" (Some "<Ctrl><Shift>C");
-    qitem "Print" (Some "<Ctrl><Shift>P");
-    qitem "About" (Some "<Ctrl><Shift>A");
-    qitem "Locate" (Some "<Ctrl><Shift>L");
-    qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
+    qitem "Search" "K";
+    qitem "Check" "C";
+    qitem "Print" "P";
+    qitem "About" "A";
+    qitem "Locate" "L";
+    qitem "Print Assumptions" "N";
   ];
-  user_queries_items queries_menu "Query" user_queries#get "<Ctrl><Shift>";
+  user_queries_items queries_menu "Query" user_queries#get;
 
   menu tools_menu [
     item "Tools" ~label:"_Tools";
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 6bb19c638..f2945a5e0 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -315,6 +315,9 @@ let modifier_for_tactics =
 let modifier_for_display =
   new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
 
+let modifier_for_queries =
+  new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string)
+
 let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
 let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
 let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
@@ -852,6 +855,9 @@ let configure ?(apply=(fun () -> ())) () =
   let modifier_for_display =
     pmodifiers "Modifiers for View Menu" modifier_for_display
   in
+  let modifier_for_queries =
+    pmodifiers "Modifiers for Queries Menu" modifier_for_queries
+  in
   let modifiers_valid =
     pmodifiers ~all:true "Allowed modifiers" modifiers_valid
   in
@@ -977,7 +983,7 @@ let configure ?(apply=(fun () -> ())) () =
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
         modifier_for_templates; modifier_for_display; modifier_for_navigation;
-        user_queries]);
+        modifier_for_queries; user_queries]);
      Section("Misc", Some `ADD,
        misc)]
   in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ebcff2080..426b0a328 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -65,6 +65,7 @@ val modifier_for_navigation : string preference
 val modifier_for_templates : string preference
 val modifier_for_tactics : string preference
 val modifier_for_display : string preference
+val modifier_for_queries : string preference
 val modifiers_valid : string preference
 val cmd_browse : string preference
 val cmd_editor : string preference