]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
added records
[helm.git] / helm / matita / matitaGui.ml
index 34238f80d4e66cb199d7c0f232f4b6dfb0c29f65..abab0f7932cf2559a771da7f031222a715f18f49 100644 (file)
@@ -174,7 +174,7 @@ class gui () =
         | Some f -> 
               script#reset (); 
               script#loadFrom f; 
-              console#message ("'"^f^"' loaded.");
+              console#message ("'"^f^"' loaded.\n");
               self#_enableSaveTo f
         | None -> ()
       in
@@ -289,7 +289,8 @@ class gui () =
         initializer
           self#check_widgets ();
           let combo_widget = combo#coerce in
-          uriHBox#add combo_widget
+          uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
+          combo#entry#misc#grab_focus ()
         method browserUri = combo
       end