X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=abab0f7932cf2559a771da7f031222a715f18f49;hb=cd8b75e8d2fd842e022352af0c01954985a924fc;hp=a17b9bfb16942a8c62ba3cda6f6a186f8824fbad;hpb=fd372e069bbcaa96dc5b2eef04f341b28850d726;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index a17b9bfb1..abab0f793 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -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 @@ -183,7 +183,7 @@ class gui () = match self#chooseFile ~ok_not_exists:true () with | Some f -> script#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); self#_enableSaveTo f | None -> () in @@ -192,7 +192,7 @@ class gui () = | None -> saveAsScript () | Some f -> (s ())#saveTo f; - console#message ("'"^f^"' saved."); + console#message ("'"^f^"' saved.\n"); in let newScript () = (s ())#reset (); disableSave () in let cursor () = @@ -289,8 +289,8 @@ class gui () = initializer self#check_widgets (); let combo_widget = combo#coerce in - browserHBox#add combo_widget; - browserHBox#reorder_child combo_widget ~pos:6 + uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; + combo#entry#misc#grab_focus () method browserUri = combo end