...

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 827bdf375ceee5ed004ecc62379eaacd347ef707..1fe78046e38d6bb7d70fe0ab4994f0632a522f53 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -843,6 +843,8 @@ class gui () =
               source_view#source_buffer#begin_not_undoable_action ();
               script#loadFromFile f; 
               source_view#source_buffer#end_not_undoable_action ();
+              source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
+              source_view#buffer#place_cursor source_view#buffer#start_iter;
               console#message ("'"^f^"' loaded.\n");
               self#_enableSaveTo f
           | None -> ()
@@ -1134,6 +1136,8 @@ class gui () =
       source_view#source_buffer#begin_not_undoable_action ();
       script#loadFromFile content;
       source_view#source_buffer#end_not_undoable_action ();
+      source_view#buffer#move_mark `INSERT source_view#buffer#start_iter;
+      source_view#buffer#place_cursor source_view#buffer#start_iter;
       console#message ("'"^file^"' loaded.");
       self#_enableSaveTo file
       
@@ -1166,7 +1170,6 @@ class gui () =
           self#check_widgets ();
           let combo_widget = combo#coerce in
           uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
-          self#toplevel#set_transient_for main#toplevel#as_window;
           combo#misc#grab_focus ()
         method browserUri = combo
       end