X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c6a8aef6af103091bf1a6cd350c6d3c8c504e347;hpb=b5c8067f175cd5bf1162ca938712ea671ac4514c;p=helm.git

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 *)