From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Dec 2010 17:42:07 +0000 (+0000)
Subject: More code clean-up.
X-Git-Tag: make_still_working~2616
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f5afdc73a5331357c3410858d5202a98832e59b;p=helm.git

More code clean-up.
---

diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade
index 28a5e609f..23e411bb0 100644
--- 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 0bea9c43f..a9ba50844 100644
--- 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 c9f4f71ff..5ced23d9e 100644
--- 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 ff381b887..5b40bb419 100644
--- 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 ()