diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:40:33 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:40:33 +0200 |
| commit | c6d5f9c39b3e12f58745c22eade90d34548b6283 (patch) | |
| tree | e42a27483494c7f03844f657609c9ff691f8603d /ide/preferences.ml | |
| parent | abd469790c2e144f693e1b21c5cdc03aee178e6d (diff) | |
Add an option to configure the modifier for Queries.
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 8 |
1 files changed, 7 insertions, 1 deletions
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 |