ocaml 3.09 transition

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c6a8aef6af103091bf1a6cd350c6d3c8c504e347..fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e 100644 (file)
--- 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 *)