indexing description: "[ A checkbox which can be selected or deselected. Events: - `checked_event': Triggered when the checkbox is checked. Passes no arguments. - `unchecked_event': Triggered when the checkbox is unchecked. Passes no arguments. ]" date: "$Date$" revision: "$Revision$" class EM_CHECKBOX inherit EM_WIDGET create make_empty, make_from_text feature {NONE} -- Initialisation make_empty is -- Initialise checkbox with empty text. do make_from_text ("") ensure empty_text: text.count = 0 end make_from_text (a_text: STRING) is -- Initialise checkbox with `a_text' as text. require a_text_not_void: a_text /= Void do text := a_text create checked_event create unchecked_event make_void_surface resize_to_optimal_dimension mouse_button_down_event.subscribe (agent handle_mouse_button_down) mouse_button_up_event.subscribe (agent handle_mouse_button_up) ensure text_set: text = a_text end delegate_factory: FUNCTION [ANY, TUPLE [], like delegate] is -- Factory to create default delegate do Result := theme_delegates.checkbox_delegate_factory end feature -- Access text: STRING -- Text of `Current' feature -- Status report is_checked: BOOLEAN -- Is `Current' selected? feature -- Status setting set_checked is -- Set `Current' to selected status. -- This will trigger a checked event. do is_checked := True Component_event_queue.add_event (checked_event, []) set_changed ensure checked: is_checked changed: is_changed end set_unchecked is -- Set `Current' to unchecked status. -- This will trigger a unchecked event. do is_checked := False Component_event_queue.add_event (unchecked_event, []) set_changed ensure not_checked: not is_checked changed: is_changed end feature -- Element change set_text (a_text: like text) is -- Set `text' to `a_text'. require a_text_not_void: a_text /= Void do text := a_text set_changed ensure text_set: text = a_text changed: is_changed end feature -- Events checked_event: EM_EVENT_CHANNEL [TUPLE []] -- Checkbox checked event unchecked_event: EM_EVENT_CHANNEL [TUPLE []] -- Checkbox unchecked event feature {NONE} -- Mouse management is_mouse_down: BOOLEAN -- Is mouse button currently down? handle_mouse_button_down (event: EM_MOUSEBUTTON_EVENT) is -- Handle mouse button down event. do is_mouse_down := True end handle_mouse_button_up (event: EM_MOUSEBUTTON_EVENT) is -- Handle mouse button up event. do if is_mouse_down then if is_checked then set_unchecked else set_checked end end is_mouse_down := False end invariant text_not_void: text /= Void checked_event_not_void: checked_event /= Void unchecked_event_not_void: unchecked_event /= Void end