X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=8d82497654a94546595fab91019846957ca43a5b;hb=dc861d214cb992a898f81752614201b8074eef12;hp=90826e98f9f6e72265313c65495798849b5913a3;hpb=de4be1b51749200158ffb1984d6da3004b3690a9;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 90826e98f..8d8249765 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -487,7 +487,6 @@ class gui () =
         | `DELETE_EVENT -> return None));
         (* menus *)
       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
-      main#helpMenu#set_right_justified true;
         (* console *)
       let adj = main#logScrolledWin#vadjustment in
         ignore (adj#connect#changed
@@ -614,7 +613,8 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"))
+          (source_buffer#get_iter_at_mark (`NAME "locked"));
+        source_view#misc#grab_focus ()
       in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in