class interface BITMAP_DEVICE creation make (model: GRAPHIC_DEVICE) -- Create bitmap/memory device. require valid: model /= Void and model.is_ready; supported: model.capabilities.has_raster_bitmap feature(s) from MEMORY -- Removal : dispose -- Finalisation. full_collect -- Force a full collection cycle if garbage collection is -- enabled; do nothing otherwise. feature(s) from GRAPHIC_DEVICE -- Access is_ready: BOOLEAN -- Is the device ready? prepare -- Device is ready at creation. require invalid: not is_ready ensure ready_at_creation: false; ready: is_ready release -- Terminate processing with this device. require ready: is_ready ensure invalid: not is_ready feature(s) from GRAPHIC_DEVICE -- Capabilities capabilities: DEVICE_CAPABILITIES -- Device capabilities. text_capabilities: TEXT_METRICS -- Text capabilities. feature(s) from GRAPHIC_DEVICE -- Coordinates conversions logical_to_device (pt: POINT): POINT -- Convert logical to device coordinates. require valid_point: pt /= Void; ready: is_ready ensure is_copy: Result /= Void device_to_logical (pt: POINT): POINT -- Convert device to logical coordinates. require valid_point: pt /= Void; ready: is_ready ensure is_copy: Result /= Void feature(s) from GRAPHIC_DEVICE -- Set drawing attributes reset -- Reset attributes. set_mapping (mode: GRAPHIC_MAPPING) -- Set mapping mode. require valid_mode: mode /= Void set_mode (mode: GRAPHIC_MODE) -- Set the current graphic mode, used to determine how the -- current pen and brush are applied. Note that it does not -- apply to text. require valid_mode: mode /= Void; raster: capabilities.is_raster_display -- ? set_background_color (clr: COLOR) -- Set the current background color, used by the device -- for text drawn with a background area, and to fill -- gaps between some styled lines (using SIMPLE_PEN) -- for instance. require valid: clr /= Void set_font (ft: FONT) -- Set current font. require valid_font: ft /= Void set_brush (br: BRUSH) -- Set current brush require valid_brush: br /= Void set_pen (pn: PEN) -- Set current pen. require valid_pen: pn /= Void set_palette (pal: PALETTE) -- Set current palette. require valid_pal: pal /= Void; possible: is_ready implies capabilities.has_palette; -- ? is_ready implies pal.size <= capabilities.palette_size good_size: feature(s) from GRAPHIC_DEVICE -- Clipping is_point_visible (pt: POINT): BOOLEAN -- Is point in the current clipping area? require valid_point: pt /= Void; ready: is_ready is_rectangle_visible (rect: RECTANGLE): BOOLEAN -- Does this rectangle has an intersection with the -- current clipping area? require valid_rectangle: rect /= Void; ready: is_ready feature(s) from GRAPHIC_DEVICE -- Actions draw (obj: DRAWABLE) -- Draw the drawable object. require valid_object: obj /= Void; ready: is_ready feature(s) from GRAPHIC_DEVICE -- Text metrics text_extent (obj: DRAWABLE_TEXT): RECTANGLE -- Return the size of the bounding rectangle of the -- text, as if it was drawn now. require valid_object: obj /= Void; ready: is_ready ensure is_copy: Result /= Void; origin: Result.lower.is_origin character_width (ch: CHARACTER): INTEGER -- Get witdh of a single character, as if it was drawn now. require ready: is_ready feature(s) from GRAPHIC_DEVICE -- Colour get_point_color (pt: POINT): COLOR -- Get pixel colour. require ready: is_ready; valid: pt /= Void; raster: capabilities.is_raster_display ensure void_if_outside: -- color = Void if outside clipping rectangle feature(s) from BITMAP_DEVICE -- Status width: INTEGER -- Width of the bitmap, in pixels. require ready: is_ready ensure ok: Result >= 0 height: INTEGER -- Height of the bitmap, in pixels. require ready: is_ready ensure ok: Result >= 0 feature(s) from BITMAP_DEVICE -- Operations set_size (w, h: INTEGER) -- Set the size of this bitmap device (the previous image is lost) -- to a width of w and height h, in pixels. require ready: is_ready ensure ok: w = width and h = height copy_from_device (other: GRAPHIC_DEVICE) -- Copy bitmap from other device at the position defined -- by set_position. require ready: is_ready; valid_device: other /= Void and then other.is_ready; supported: other.capabilities.has_raster_bitmap load_resource (name: STRING) -- Load bitmap from resource. require valid_name: name /= Void load (fname: STRING) -- Load bitmap from file. require valid: fname /= Void; ready: is_ready save (fname: STRING) -- Save bitmap to file. require valid: fname /= Void; ready: is_ready feature(s) from BITMAP_DEVICE -- Status set_position (tpos: POINT) -- Set target position for drawing. require valid: tpos /= Void set_mode_stretch -- Set drawing mode to stretch (adapt size when drawing). reset_mode -- Set drawing mode to copy (size in destination device -- is the same). set_mode_copy -- Set drawing mode to copy (size in destination device -- is the same). set_target (rect: RECTANGLE) -- Set target rectangle for stretching. require valid: rect /= Void invariant valid_attrib: pen /= Void and brush /= Void and mapping /= Void; valid_caps: capabilities /= Void and then text_capabilities /= Void; bmp: bitmap /= Void; end of BITMAP_DEVICE