class interface DRAWABLE_UNICODE_TEXT creation make -- Create/initialise text object. feature(s) from DRAWABLE_TEXT -- Creation make -- Create/initialise text object. feature(s) from DRAWABLE_TEXT -- Creation reset -- Create/initialise text object. feature(s) from DRAWABLE_TEXT -- Text set_text (txt: STRING) -- Set the text to draw. require valid_txt: txt /= Void ensure done: text.is_equal(txt) feature(s) from DRAWABLE_TEXT -- Text output specifications set_position (pt: POINT) -- Set reference point used to position the text. require valid_position: pt /= Void ensure done: pos_x = pt.x and pos_y = pt.y set_area (rpos: RECTANGLE) -- Set area which will be filled with background colour, -- assumes window device in text mode. -- (Default: none, text output transparent). require ok: rpos /= Void ensure done: has_area; area_ok: area_x = rpos.lower.x and area_y = rpos.lower.y and area_xp = rpos.upper.x + 1 and area_yp = rpos.upper.y + 1 set_color (clr: COLOR) -- Set text colour. require valid_color: clr /= Void set_justification (justif: INTEGER) -- Set justification. The justification value is the width -- to be added to the string at the break characters. require valid: justif >= 0 ensure done: justification = justif set_intercharacter_spacing (ispace: INTEGER) -- Set intecharacter spacing (default: 0). require valid: ispace >= 0 ensure done: intercharacter_spacing = ispace feature(s) from DRAWABLE_TEXT -- Alignment align_top -- Reference point aligned with the top of the bounding rectangle (default). align_baseline -- Reference point aligned with the base line of the text. align_bottom -- Reference point aligned with the bottom of the bounding rectangle. align_left -- Reference point horizontally aligned with the left of the bounding rectangle (Default). align_center -- Reference point aligned with the centre of the bounding rectangle. align_right -- Reference point horizontally aligned with the right of the bounding rectangle. feature(s) from DRAWABLE_UNICODE_TEXT set_character_map (map: ARRAY[INTEGER]) -- Set the character map used to convert 8-bit characters to -- UNICODE. map.item (input_char.code) is the Unicode character -- code. This must be set before any drawing takes place. -- (this setting is not changed when reset is called). require ok: map /= Void; map_size: map.lower = 0 and map.upper = 255; -- 0x00 -> 0xFF -- for_all i, 0 <= map.item (i) <= 65535 char_size: invariant valid: text /= Void; narrow_characters: -- CHARACTER.code <= 255 end of DRAWABLE_UNICODE_TEXT