X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=1fe78046e38d6bb7d70fe0ab4994f0632a522f53;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=827bdf375ceee5ed004ecc62379eaacd347ef707;hpb=02763a89e6351dfb7770251d0507512e3f0ddb74;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 827bdf375..1fe78046e 100644 --- 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