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