X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=abab0f7932cf2559a771da7f031222a715f18f49;hb=cd8b75e8d2fd842e022352af0c01954985a924fc;hp=d18b82d140833f1cedfdc78db10d728f6af639cb;hpb=ccca8f161bcbe57b58e651656a4a825c5227abf2;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index d18b82d14..abab0f793 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -31,6 +31,14 @@ open MatitaMisc
 
 let gui_instance = ref None ;;
 
+class type browserWin =
+  (* this class exists only because GEdit.combo_box_entry is not supported by
+   * lablgladecc :-(((( *)
+object
+  inherit MatitaGeneratedGui.browserWin
+  method browserUri: GEdit.combo_box_entry
+end
+
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
@@ -166,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
@@ -175,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
@@ -184,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 () =
@@ -275,9 +283,16 @@ class gui () =
     method main = main
 
     method newBrowserWin () =
-      let win = new browserWin () in
-      win#check_widgets ();
-      win
+      object (self)
+        inherit browserWin ()
+        val combo = GEdit.combo_box_entry ()
+        initializer
+          self#check_widgets ();
+          let combo_widget = combo#coerce in
+          uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
+          combo#entry#misc#grab_focus ()
+        method browserUri = combo
+      end
 
     method newUriDialog () =
       let dialog = new uriChoiceDialog () in