X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=08f097086fdc59540b7c9c683f3a6cf8d27b62f7;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=d18b82d140833f1cedfdc78db10d728f6af639cb;hpb=ccca8f161bcbe57b58e651656a4a825c5227abf2;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index d18b82d14..08f097086 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" ] @@ -275,9 +283,15 @@ 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#add combo_widget + method browserUri = combo + end method newUriDialog () = let dialog = new uriChoiceDialog () in