From 1fd705ca03b47c1877a7d30d687adb7700a8b7cc Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 7 Nov 2005 10:29:25 +0000 Subject: [PATCH] changed script actions keybindings: s/CTRL-XXX/CTRL-ALT-XXX/ --- helm/matita/matita.glade | 118 ++++++++++++++++++++++++++++++--------- helm/matita/matitaGui.ml | 19 ++----- 2 files changed, 97 insertions(+), 40 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 6b951b21d..6ddd786b9 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -877,7 +877,7 @@ - + True gtk-new 1 @@ -898,7 +898,7 @@ - + True gtk-open 1 @@ -919,7 +919,7 @@ - + True gtk-save 1 @@ -940,7 +940,7 @@ - + True gtk-save-as 1 @@ -961,7 +961,7 @@ - + True gtk-execute 1 @@ -988,7 +988,7 @@ - + True gtk-quit 1 @@ -1023,7 +1023,7 @@ - + True gtk-undo 1 @@ -1045,7 +1045,7 @@ - + True gtk-redo 1 @@ -1072,7 +1072,7 @@ - + True gtk-cut 1 @@ -1093,7 +1093,7 @@ - + True gtk-copy 1 @@ -1114,7 +1114,7 @@ - + True gtk-paste 1 @@ -1134,7 +1134,7 @@ True - + True gtk-delete 1 @@ -1175,7 +1175,7 @@ - + True gtk-find-and-replace 1 @@ -1215,6 +1215,76 @@ + + + True + _Script + True + + + + + + + True + Execute 1 phrase + True + + + + + + + True + Retract 1 phrase + True + + + + + + + True + + + + + + True + Execute all + True + + + + + + + True + Restart + True + + + + + + + True + + + + + + True + Execute until cursor + True + + + + + + + + True @@ -1274,7 +1344,7 @@ - + True gtk-zoom-in 1 @@ -1296,7 +1366,7 @@ - + True gtk-zoom-out 1 @@ -1317,7 +1387,7 @@ - + True gtk-zoom-100 1 @@ -1369,7 +1439,7 @@ True - + True gtk-about 1 @@ -2037,11 +2107,10 @@ True - restart (Ctrl+Home) + Restart True GTK_RELIEF_NONE True - @@ -2073,11 +2142,10 @@ True - go back 1 phrase (Ctrl+Page Up) + Retract 1 phrase True GTK_RELIEF_NONE True - @@ -2109,7 +2177,7 @@ True - execute until point + Execute until point True GTK_RELIEF_NONE True @@ -2144,11 +2212,10 @@ True - go forward 1 phrase (Ctrl+Page Down) + Execute 1 phrase True GTK_RELIEF_NONE True - @@ -2180,11 +2247,10 @@ True - execute all (Ctrl+End) + Execute all True GTK_RELIEF_NONE True - diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index c6a8aef6a..fe113743b 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -702,25 +702,16 @@ class gui () = connect_button main#scriptRetractButton retract; connect_button main#scriptTopButton top; connect_button main#scriptBottomButton bottom; - connect_key GdkKeysyms._Down advance; - connect_key GdkKeysyms._Up retract; - connect_key GdkKeysyms._Home top; - connect_key GdkKeysyms._End bottom; connect_button main#scriptJumpButton jump; + connect_menu_item main#scriptAdvanceMenuItem advance; + connect_menu_item main#scriptRetractMenuItem retract; + connect_menu_item main#scriptTopMenuItem top; + connect_menu_item main#scriptBottomMenuItem bottom; + connect_menu_item main#scriptJumpMenuItem jump; connect_menu_item main#openMenuItem loadScript; connect_menu_item main#saveMenuItem saveScript; connect_menu_item main#saveAsMenuItem saveAsScript; connect_menu_item main#newMenuItem newScript; - connect_key GdkKeysyms._period - (fun () -> - source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) - ".\n"; - advance ()); - connect_key GdkKeysyms._Return - (fun () -> - source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) - "\n"; - advance ()); (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) -- 2.39.2