class interface STD_COMBOBOX[G->LISTBOX_ITEM] creation make (p: WINDOW) -- Create combobox. require valid_parent: p /= Void make_unsorted (p: WINDOW) -- Create combobox whose list is unsorted. require valid: p /= Void feature(s) from LISTBOX -- Manage associated list add_list (lst: DS_LINEAR[G]) -- Add items to the list box. require valid_list: lst /= Void add_item (item: G) -- Add item to the list. require valid_item: item.is_valid remove_all -- Reset list. ensure empty: items.is_empty feature(s) from LISTBOX -- Selection has_selection: BOOLEAN -- Is an item selected? selected_item: G -- Currently selected item. require select_ok: has_selection has_item (itm: G): BOOLEAN -- Is itm in our list? select_item (new: G) -- Mark new as selected. require has: has_item(new) feature(s) from LISTBOX -- Commands set_select_command (gc: GUI_COMMAND) -- Set when_selected command. require nothing: -- Void means no command ensure keep_reference: select_command = gc set_execute_command (gc: GUI_COMMAND) -- Set when_execute command. require nothing: -- Void means no command ensure keep_reference: execute_command = gc feature(s) from CONTROL -- Implementation self: CHILD_WINDOW -- Associated child window. feature(s) from CONTROL -- Dialog box has_dialog_box: BOOLEAN -- Check if control has associated dialog box. dialog_box: DIALOG -- Associated dialog which holds the control. require has_dialog: has_dialog_box ensure valid: Result /= Void feature(s) from CONTROL -- Control's font set_font (ft: FONT) -- Set control font. require valid_font: ft /= Void feature(s) from CONTROL -- Position, independent indep_size: RECTANGLE -- Control size using dialog coordinates. ensure is_copy: -- can be modified. indep_set_size (rect: RECTANGLE) -- Set listbox size in independent coordinates. -- Note: Control's height is set by the operating system, -- so the height is ignored. require valid: rect /= Void ensure done: rect.is_equal(indep_size); height_unchanged: -- height ignored feature(s) from DIALOG_ELEMENT -- Device independent positioning indep_set_point (p: POINT) -- Set upper-left point of element using device independent units. require valid_point: p /= Void indep_set_width (wi: INTEGER) -- Set element's width using device independent units. require valid: wi >= 0 indep_set_height (he: INTEGER) -- Set element's height using device independent units. require valid: he >= 0 feature(s) from DIALOG_ELEMENT -- Relative positioning place_right (other: DIALOG_ELEMENT) -- Place the current element to the right of other. require valid_other: other /= Void place_left (other: DIALOG_ELEMENT) -- Place the current element to the left of other. require valid_other: other /= Void place_above (other: DIALOG_ELEMENT) -- Place the current element above other. require valid_other: other /= Void place_under (other: DIALOG_ELEMENT) -- Place the current element under other. require valid_other: other /= Void place_just_under (other: DIALOG_ELEMENT) -- Place the current element exactly under 'other'. same_width (other: DIALOG_ELEMENT) -- Set the current element width to other's. require valid_other: other /= Void same_height (other: DIALOG_ELEMENT) -- Set the current element height to be the same as other's. require valid_other: other /= Void align_left (other: DIALOG_ELEMENT) -- Align left side of this element with the -- left side of other. require ok: other /= Void align_right (other: DIALOG_ELEMENT) -- Align the right side of this element with the right -- side of other. require ok: other /= Void align_top (other: DIALOG_ELEMENT) -- Align the top of this element with top of other. require ok: other /= Void align_bottom (other: DIALOG_ELEMENT) -- Align the bottom of this element with bottom of other. require ok: other /= Void feature(s) from STRINGBOX contents: STRING -- Edited string. ensure plain: contents /= Void set_contents (s: STRING) -- Change editable string. require valid_string: s /= Void ensure contents_set: contents.is_equal(s) feature(s) from STRINGBOX set_command (gc: GUI_COMMAND) -- Set when_changed command. require nothing: -- Void means no command ensure keep_reference: command = gc feature(s) from CLIPBOARD_OBJECT clipboard_has_selection: BOOLEAN -- Has current selection? cut_selection -- Cut selection. require has_selection: clipboard_has_selection copy_selection -- Copy current selection. require has_selection: clipboard_has_selection paste_clipboard -- Paste clipboard to object. ensure has_selection: clipboard_has_selection delete_selection -- Delete selection. require has_selection: clipboard_has_selection select_all -- Select everything. feature(s) from STD_DROPDOWN_LISTBOX -- Size. set_popup_list_height (h: INTEGER) -- Set the height of the popup list require valid_height: h > 0 default_size -- Set size to default. invariant list_init: items /= Void; end of STD_COMBOBOX[G->LISTBOX_ITEM]