More code clean-up.

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index 28a5e609f44a920e49cc9ca805d00ecb567a9688..23e411bb039f13277c82fe24c9e8f853417114a4 100644 (file)
--- a/matita/matita/matita.glade
+++ b/matita/matita/matita.glade
@@ -212,7 +212,15 @@
                       <widget class="GtkHBox" id="UriHBox">
                         <property name="visible">True</property>
                         <child>
-                          <placeholder/>
+                          <widget class="GtkEntry" id="browserUri">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="has_focus">True</property>
+                            <property name="invisible_char">&#x25CF;</property>
+                          </widget>
+                          <packing>
+                            <property name="position">0</property>
+                          </packing>
                         </child>
                       </widget>
                       <packing>

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 0bea9c43f6a1531c5bb6d927544e8ecc2e873372..a9ba508441914f1bd086bb901823da27e7a97b3e 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -106,14 +106,6 @@ let interactive_uri_choice
   end
 
 
-class type browserWin =
-  (* this class exists only because GEdit.combo_box_entry is not supported by
-   * lablgladecc :-(((( *)
-object
-  inherit MatitaGeneratedGui.browserWin
-  method browserUri: GEdit.entry
-end
-
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
@@ -1052,17 +1044,6 @@ class gui () =
     method private findRepl = findRepl
     method main = main
 
-    method newBrowserWin () =
-      object (self)
-        inherit browserWin ()
-        val combo = GEdit.entry ()
-        initializer
-          let combo_widget = combo#coerce in
-          uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
-          combo#misc#grab_focus ()
-        method browserUri = combo
-      end
-
     method private addKeyBinding key callback =
       List.iter (fun evbox -> add_key_binding key callback evbox)
         keyBindingBoxes

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index c9f4f71ff21737d06511d8627ecc089a1bdc18f1..5ced23d9edae6cef9cbe216785d1fa19eaf7ab05 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -23,24 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
-class type browserWin =
-object
-  inherit MatitaGeneratedGui.browserWin
-  method browserUri: GEdit.entry
-end
-
 class type gui =
 object
     (** {2 Access to singleton instances of lower-level GTK widgets} *)
   method main: MatitaGeneratedGui.mainWin
 
-    (** {2 Dialogs instantiation}
-     * methods below create a new window on each invocation. You should
-     * remember to destroy windows after use *)
-  method newBrowserWin: unit -> browserWin
-
     (** {2 Utility methods} *)
-
   method newScript: unit -> unit
   method loadScript: string -> unit
 end

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index ff381b88787df8c80503c83bcdb1a73275c0dba0..5b40bb4195ed2795b1dd6b2cbc563b34d38172e9 100644 (file)
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -238,7 +238,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
   let gui = MatitaMisc.get_gui () in
-  let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
+  let win = new MatitaGeneratedGui.browserWin () in
+  let _ = win#browserUri#misc#grab_focus () in
   let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
   let searchText = 
     GSourceView2.source_view ~auto_indent:false ~editable:false ()