From: Claudio Sacerdoti Coen 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 @@ True - + + True + True + True + + + + 0 + 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 ()