fixed whelp bar

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5045f36d1aa5148bd3ec80c2f3c3a7fa4b46ed26..f3b531fb285dee2bc6e60e46044fe1e5177acc12 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -254,30 +254,6 @@ class gui () =
 
     method newBrowserWin () =
       let win = new browserWin () in
-      win#whelpImage2#set_file "icons/whelp.png";
-      win#whelpBarToggleButton#set_active false;   
-      win#whelpBarBox#misc#hide ();
-      win#mathOrListNotebook#set_show_tabs false;
-      connect_toggle_button win#whelpBarToggleButton 
-        (fun () -> 
-          if win#whelpBarToggleButton#active then
-            win#whelpBarBox#misc#show ()
-          else
-            win#whelpBarBox#misc#hide ());
-      let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
-      let combo,(combo_store,combo_column) = 
-        GEdit.combo_box_text ~strings:queries () 
-      in
-      combo#set_active 0;
-      win#comboVbox#add (combo :> GObj.widget);
-      let start_query () = 
-        let query = String.lowercase (List.nth queries combo#active) in
-        let input = win#queryInputText#text in
-        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
-        (MatitaScript.instance ())#advance ~statement ()
-      in
-      ignore(win#queryInputText#connect#activate ~callback:start_query);
-      ignore(combo#connect#changed ~callback:start_query);
       win#check_widgets ();
       win