diff options
| author | Hugo Herbelin | 2018-11-03 17:07:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-10 12:04:40 +0200 |
| commit | 00603110458a40b1fe4bd4d51545a3e9b685e83c (patch) | |
| tree | 6ad94df881a9aa2acef8ded3de177cd2cb644158 /ide | |
| parent | 0cb8482b51f25b2f705f4da28f08424f48fa9c93 (diff) | |
Using GTK+ PRIMARY to factorize CoqIDE keys between MacOS and others.
This concerns zooming, undoing, displaying preferences.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/MacOS/default_accel_map | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6bcf3b438f..4093d2012b 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -47,7 +47,7 @@ (gtk_accel_path "<Actions>/View/Display notations" "<Shift><Control>n") ; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic left" "") -(gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u") +; (gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u") ; (gtk_accel_path "<Actions>/Templates/Template Infix" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "") @@ -219,7 +219,7 @@ ; (gtk_accel_path "<Actions>/Templates/Template Remark" "") ; (gtk_accel_path "<Actions>/Templates/Template Set Undo" "") ; (gtk_accel_path "<Actions>/Templates/Template Inductive" "") -(gtk_accel_path "<Actions>/Edit/Preferences" "<Primary>VoidSymbol") +; (gtk_accel_path "<Actions>/Edit/Preferences" "<Primary>,") ; (gtk_accel_path "<Actions>/Export/Html" "") ; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "") diff --git a/ide/coqide.ml b/ide/coqide.ml index fb08195308..e0ae18dddc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1016,7 +1016,7 @@ let build_ui () = menu edit_menu [ item "Edit" ~label:"_Edit"; - item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO + item "Undo" ~accel:"<Primary>u" ~stock:`UNDO ~callback:(cb_on_current_term (fun t -> t.script#undo ())); item "Redo" ~stock:`REDO ~callback:(cb_on_current_term (fun t -> t.script#redo ())); @@ -1035,7 +1035,7 @@ let build_ui () = ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ())); item "External editor" ~label:"External editor" ~stock:`EDIT ~callback:(External.editor ~parent:w); - item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES + item "Preferences" ~accel:"<Primary>comma" ~stock:`PREFERENCES ~callback:(fun _ -> begin try Preferences.configure ~apply:refresh_notebook_pos w @@ -1053,19 +1053,19 @@ let build_ui () = item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right" ~stock:`GO_FORWARD ~callback:(fun _ -> notebook#next_page ()); - item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus") + item "Zoom in" ~label:"_Zoom in" ~accel:("<Primary>plus") ~stock:`ZOOM_IN ~callback:(fun _ -> let ft = Pango.Font.from_string text_font#get in Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale); text_font#set (Pango.Font.to_string ft); save_pref ()); - item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus") + item "Zoom out" ~label:"_Zoom out" ~accel:("<Primary>minus") ~stock:`ZOOM_OUT ~callback:(fun _ -> let ft = Pango.Font.from_string text_font#get in Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale); text_font#set (Pango.Font.to_string ft); save_pref ()); - item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0") + item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Primary>0") ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit); toggle_item "Show Toolbar" ~label:"Show _Toolbar" ~active:(show_toolbar#get) |