class interface STD_LABEL creation make (p: WINDOW) -- Create standard simple label (left justified, one-line). require valid_parent: p /= Void make_left (p: WINDOW) -- Create label with left-aligned, wordwrapped text. require valid: p /= Void make_center (p: WINDOW) -- Create label with centre centred and wordwrapped text. require valid: p /= Void feature(s) from DIALOG_ELEMENT -- Parent 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 DIALOG_ELEMENT -- Device independent positioning indep_size: RECTANGLE -- Control size using dialog coordinates. ensure is_copy: -- can be modified. indep_set_size (sz: RECTANGLE) -- Set control size using dialog coordinates. require valid: sz /= Void ensure done: sz.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 CONTROL -- Implementation self: CHILD_WINDOW -- Associated child window. feature(s) from CONTROL -- Control's font set_font (ft: FONT) -- Set control font. require valid_font: ft /= Void feature(s) from STD_LABEL -- Label set_label (str: STRING) -- Set the label name which will be displayed. require valid: str /= Void adapt_width -- Adapt width to label text. -- (based on estimate in independent coordinates) end of STD_LABEL