Commit 5909ff66 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'native-shortcut-modifiers' into 'master'

Make IDE use native modifiers for shortcuts

See merge request why3/why3!399
parents 0c3d90b8 99bfe8db
......@@ -1987,6 +1987,9 @@ let hide_context_provers, add_submenu_prover =
(* Main menu *)
(*************)
(* Use the command key (⌘) for shortcuts when on mac *)
let primary_modifiers = snd (GtkData.AccelGroup.parse "<Primary>A")
let tools_accel_group = GtkData.AccelGroup.create ()
let factory = new menu_factory ~accel_path:"<Why3-Main>/" ~accel_group menubar
let context_factory = new menu_factory context_tools_menu
......@@ -2035,19 +2038,19 @@ let (_: GMenu.menu_item) =
let (_: GMenu.menu_item) =
file_factory#add_item "_Save session and files"
~modi:[`CONTROL] ~key:GdkKeysyms._S
~modi:primary_modifiers ~key:GdkKeysyms._S
~tooltip:"Save the current proof session and the source files"
~callback:(fun () -> save_sources(); send_request Save_req)
let (_: GMenu.menu_item) =
file_factory#add_item "Save all and _Refresh session"
~modi:[`CONTROL] ~key:GdkKeysyms._R
~modi:primary_modifiers ~key:GdkKeysyms._R
~tooltip:"Save the current proof session and the source files, then refresh the proof session with updated source files."
~callback:save_and_reload
let (_: GMenu.menu_item) =
file_factory#add_item "_Quit"
~modi:[`CONTROL] ~key:GdkKeysyms._Q
~modi:primary_modifiers ~key:GdkKeysyms._Q
~tooltip:"See the Preferences for setting the policy on automatic file saving at exit."
~callback:exit_function_safe
......@@ -2126,13 +2129,13 @@ let edit_factory = new menu_factory edit_menu ~accel_path:"<Why3-Main>/Edit/" ~a
let (_: GMenu.menu_item) =
edit_factory#add_item "Search forward"
~modi:[`CONTROL] ~key:GdkKeysyms._F
~modi:primary_modifiers ~key:GdkKeysyms._F
~tooltip:"Search in the source file."
~callback:(search_forward ~forward:true)
let (_: GMenu.menu_item) =
edit_factory#add_item "Search backward"
~modi:[`CONTROL] ~key:GdkKeysyms._B
~modi:primary_modifiers ~key:GdkKeysyms._B
~tooltip:"Search backward in the source file."
~callback:(search_forward ~forward:false)
......@@ -2232,13 +2235,13 @@ let find_cursor_ident, get_back_loc =
let (_: GMenu.menu_item) =
edit_factory#add_item "Find cursor ident"
~modi:[`CONTROL] ~key:GdkKeysyms._L
~modi:primary_modifiers ~key:GdkKeysyms._L
~tooltip:"This finds the definition of the ident under user cursor"
~callback:find_cursor_ident
let (_: GMenu.menu_item) =
edit_factory#add_item "Back"
~modi:[`CONTROL] ~key:GdkKeysyms._ampersand (* & *)
~modi:primary_modifiers ~key:GdkKeysyms._ampersand (* & *)
~tooltip:"After find cursor ident, return back to cursor"
~callback:get_back_loc
......@@ -2267,12 +2270,12 @@ let view_factory = new menu_factory ~accel_path:"<Why3-Main>/View/" ~accel_group
let (_ : GMenu.menu_item) =
view_factory#add_item "Enlarge font"
~modi:[`CONTROL] ~key:GdkKeysyms._plus
~modi:primary_modifiers ~key:GdkKeysyms._plus
~callback:enlarge_fonts
let (_ : GMenu.menu_item) =
view_factory#add_item "Reduce font"
~modi:[`CONTROL] ~key:GdkKeysyms._minus
~modi:primary_modifiers ~key:GdkKeysyms._minus
~callback:reduce_fonts
let (_: GMenu.menu_item) =
......@@ -2299,7 +2302,7 @@ let (_: GMenu.menu_item) =
let (_: GMenu.menu_item) =
view_factory#add_item "Go to parent node"
~modi:[`CONTROL] ~key:GdkKeysyms._Left
~modi:primary_modifiers ~key:GdkKeysyms._Left
~callback:move_current_row_selection_to_parent
let (_: GMenu.menu_item) =
......@@ -2308,17 +2311,17 @@ let (_: GMenu.menu_item) =
let (_: GMenu.menu_item) =
view_factory#add_item "Select next unproven goal"
~modi:[`CONTROL] ~key:GdkKeysyms._Right
~modi:primary_modifiers ~key:GdkKeysyms._Right
~callback:(fun () -> move_to_next_unproven_node_id Clever)
let (_: GMenu.menu_item) =
view_factory#add_item "Go down (skipping proved goals)"
~modi:[`CONTROL] ~key:GdkKeysyms._Down
~modi:primary_modifiers ~key:GdkKeysyms._Down
~callback:(fun () -> move_to_next_unproven_node_id Next)
let (_: GMenu.menu_item) =
view_factory#add_item "Go up (skipping proved goals)"
~modi:[`CONTROL] ~key:GdkKeysyms._Up
~modi:primary_modifiers ~key:GdkKeysyms._Up
~callback:(fun () -> move_to_next_unproven_node_id Prev)
(* "Help" menu items *)
......@@ -2536,12 +2539,12 @@ let () = tools_factory#add_separator ()
let copy_item =
tools_factory#add_item "Copy node"
~modi:[`CONTROL] ~key:GdkKeysyms._C
~modi:primary_modifiers ~key:GdkKeysyms._C
~tooltip:"Copy the current node"
let paste_item =
tools_factory#add_item "Paste node"
~modi:[`CONTROL] ~key:GdkKeysyms._V
~modi:primary_modifiers ~key:GdkKeysyms._V
~tooltip:"Paste the copied node below the current node"
(* complete the contextual menu (but only after provers and strategies, hence the function) *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment