deferred class interface PUSH_BUTTON feature(s) from DIALOG_ELEMENT -- Parent has_dialog_box: BOOLEAN -- Does the object has a valid corresponding dialog? dialog_box: DIALOG -- The object which uses dialog elements. require has_dialog: has_dialog_box ensure valid: Result /= Void feature(s) from DIALOG_ELEMENT -- Device independent positioning indep_size: RECTANGLE -- Size of element using device independent coordinates. ensure is_copy: -- can be modified. indep_set_size (r: RECTANGLE) -- Set element's size in device independent coordinates. require valid: r /= Void ensure done: r.is_equal(indep_size) 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 BUTTON -- Status set_label (label: STRING) -- Set the button's displayed label. require valid: label /= Void feature(s) from BUTTON -- Command set_command (gc: GUI_COMMAND) -- Set when_executed command. require nothing: -- Void means no command ensure keep_reference: command = gc feature(s) from PUSH_BUTTON -- Status is_down: BOOLEAN -- Is the button down? set_down (newstat: BOOLEAN) -- Set the button 'pushed' state. ensure set: is_down = newstat feature(s) from PUSH_BUTTON -- Positioning center -- Place button at the centre of the dialog (as -- it would be when optimally arranged). require db: has_dialog_box left_of_center -- Place button at the left of the centre of the -- dialog (as it would be when optimally arranged). require db: has_dialog_box right_of_center -- Place button at the right of the centre of the -- dialog (as it would be when optimaly arranged). require db: has_dialog_box feature(s) from PUSH_BUTTON -- Default status is_default: BOOLEAN -- Is the button the default push button? (thick border) set_default (db: BOOLEAN) -- Set the push button to default status. ensure done: db = is_default feature(s) from PUSH_BUTTON -- Command execute -- Simulate button selection. end of deferred PUSH_BUTTON