- 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
+ 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