class interface BITMAP_BUTTON

creation
   make (pw: WINDOW)
      --  Create bitmap button.


feature(s) from BUTTON
   --  Status

   set_label (str: STRING)
      --  Label unimplemented for bitmap buttons.

      require
         valid: str /= Void
      ensure
         unimplemented: false

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 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 PUSH_BUTTON
   --  Status

   is_down: BOOLEAN
      --  Is button down?


   set_down (down: BOOLEAN)
      --  Change button status.

      ensure
         set: is_down = down

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 this button the default button?


   set_default (dft: BOOLEAN)
      --  Change default status.

      ensure
         done: dft = is_default

feature(s) from PUSH_BUTTON
   --  Command

   execute
      --  Simulate button selection.


feature(s) from CONTROL
   --  Implementation

   self: CHILD_WINDOW
      --  Associated child window.


feature(s) from CONTROL
   --  Control's font

   set_font (ft: FONT)
      --  Set control's font.

      require
         valid_font: ft /= Void

feature(s) from BITMAP_BUTTON
   set_bitmap (bmp: BITMAP_DEVICE)
      --  Set associated bitmap.

      require
         ok: bmp /= Void
      ensure
         keep_reference: bitmap = bmp

   set_resource (name: STRING)
      --  Load bitmap from resource.

      require
         ok: name /= Void; --  executable.has_resource (name)
         valid_resource: 

   adjust_size
      --  Resize the button to the size of the bitmap.

      require
         has_bitmap:  --  set_bitmap or set_ressource


end of BITMAP_BUTTON