class interface PROGRESS_BAR

creation
   make (par: like parent)
      --  Create a child window.

      require
         valid: par /= Void and then par.is_valid
      ensure
         keep_reference: par = parent

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 WINDOW
   --  Window public attributes

   parent: WINDOW
      --  Parent window, it may be redefined by heirs in order to 
      --  communicate with parent window.


feature(s) from WINDOW
   --  Graphic device

   device: WINDOW_DEVICE
      --  Device used to draw in the window client area.

      ensure
         has_device: Result /= Void

feature(s) from WINDOW
   --  Window's size

   size: RECTANGLE
      --  Return the window external size relative to the client area 
      --  of the parent window for child windows.

      require
         valid: is_valid
      ensure
         valid_result: Result /= Void; --  can be modified
         is_copy: 

   client_size: RECTANGLE
      --  Return the window's client area size, in client 
      --  coordinates, that is (x, y) = (0, 0)

      require
         valid: is_valid
      ensure
         is_copy: Result /= Void; --  can be modified
 --  Result.lower.is_origin 
         lower_zero: 

   set_size (rect: RECTANGLE)
      --  Set window size. The rectangle is in screen coordinates 
      --  for a popup windown and in the parent's window client area 
      --  coordinates for a child window.

      require
         valid_window: is_valid;
         valid_rect: rect /= Void
      ensure
         size_set: rect.is_equal(size)

   set_client_size (rect: RECTANGLE)
      --  Set the client area size, in client area coordinates
      --  (so, (x, y) = (0, 0))

      require
         valid_window: is_valid;
         valid_rect: rect /= Void;
         lower_zero: rect.lower.x = 0 and rect.lower.y = 0
      ensure
         size_set: rect.is_equal(client_size)

feature(s) from WINDOW
   --  Window's text

   text: STRING
      --  Get the window text, which can be the title bar for windows 
      --  with a caption, or used for other purposes.

      require
         valid: is_valid
      ensure
         is_copy:  --  can be modified

   set_text (s: STRING)
      --  Set the window text (see 'text').

      require
         valid_window: is_valid;
         valid_string: s /= Void
      ensure
         text_set: s.is_equal(text)

feature(s) from WINDOW
   --  Associated mouse managers

   set_left_mouse_manager (track: MOUSE_HANDLER)
      --  Set associated mouse manager object for left mouse button.

      require
         void:  --  track = Void implies no tracker
      ensure
         keep_reference: lmousetrack = track --  keeps a copy of track

   set_right_mouse_manager (track: MOUSE_HANDLER)
      --  Set associated mouse manager object for right mouse button.
      --  (Default: none)

      require
         void:  --  track = Void implies no tracker
      ensure
         keep_reference: rmousetrack = track --  keeps a copy of track

feature(s) from WINDOW
   --  Window features and metrics

   is_valid: BOOLEAN
      --  Is this window currently valid? If not it has been closed 
      --  or failed to be created properly.


   is_iconic: BOOLEAN
      --  Is this window reduced to an icon?

      require
         valid: is_valid

   is_enabled: BOOLEAN
      --  Is the window able to receive user input?

      require
         valid: is_valid

   has_focus: BOOLEAN
      --  Does the window has the keyboard focus?

      require
         valid: is_valid

   is_active: BOOLEAN
      --  Is the window active?

      require
         valid: is_valid

   is_visible: BOOLEAN
      --  Is the window visible?

      require
         valid: is_valid

   is_created: BOOLEAN
      --  Has this window been created?


feature(s) from WINDOW
   --  Close status

   is_close_ready: BOOLEAN
      --  Is the window ready to be closed.
      --  If true, calling close or a close message will 
      --  destroy the window. (Default value: true)


   set_close_ready (cl: BOOLEAN)
      --  Set is_close_ready.

      ensure
         is_close_ready = cl

feature(s) from WINDOW
   --  Actions: destruction

   close
      --  Close the window, and then destroy it if 
      --  is_close_ready is true.

      require
         valid: is_valid

   destroy
      --  Destroy the window (without calling 'when_closed').

      require
         valid: is_valid
      ensure
         invalid:  --  not is_valid after when_destroyed

feature(s) from WINDOW
   --  Actions: change the way the window is displayed

   show
      --  Show the window and redraw its client area. 
      --  Can be used to unhide, or restore a window.

      require
         valid: is_valid
      ensure
         visible:  --  is_visible unless not parent.is_visible

   hide
      --  Hide the window (unhide with show).

      require
         valid: is_valid
      ensure
         hidden: not is_visible

feature(s) from WINDOW
   --  Actions: activation, focus, etc

   activate
      --  Activate the current window (make it top).

      require
         valid: is_valid
      ensure
         active: is_active

   focus
      --  Set keyboard focus to this window.

      require
         valid: is_valid
      ensure
         focus:  --  has_focus unless immediatly given to someone else

   enable
      --  Allow the user to use the window.

      require
         valid: is_valid
      ensure
         enabled: is_enabled = true

   disable
      --  Prevent the user from using the window.

      require
         valid: is_valid
      ensure
         disabled: is_enabled = false

feature(s) from WINDOW
   --  Painting the window

   paint
      --  Force a redraw of the client area of the window.

      require
         valid: is_valid

   paint_rectangle (rect: RECTANGLE)
      --  Force a redraw of the specified rectangle of the client area.

      require
         valid_window: is_valid;
         valid_rectangle: rect /= Void

   horizontal_scroll (dx: INTEGER)
      --  Scroll horizontally the client area of the window of 'dx', 
      --  and repaint the scrolled part.

      require
         valid: is_valid

   vertical_scroll (dy: INTEGER)
      --  Scroll vertically the client area of the window of 'dy', 
      --  and repaint the scrolled part.

      require
         valid: is_valid

feature(s) from CHILD_WINDOW
   --  Attached scrollbars

   horizontal_scrollbar: WINDOW_SCROLLBAR

   vertical_scrollbar: WINDOW_SCROLLBAR

feature(s) from CHILD_WINDOW
   --  Style

   set_border (hasborder: BOOLEAN)
      --  Set the window's border style:
      --  hasborder = true implies one pixel border, otherwise not.

      require
         valid: is_valid

feature(s) from CHILD_WINDOW
   --  Siblings

   is_sibling (other: WINDOW): BOOLEAN
      --  Is other an _older_ sibling of us? 
      --  (exported for preconditions)

      require
         valid_window: other /= Void;
         has_parent: parent /= Void

   next: CHILD_WINDOW
      --  Next sibling in the cycle (may be Current).


   previous: CHILD_WINDOW
      --  Previous sibling in the cycle (may be Current).


feature(s) from CHILD_WINDOW
   --  Setting up resize rules

   size_follows_parent
      --  Child window fills parent client area.


   fixed_width
      --  Width remains constant when layout changed.

      require
         valid: is_valid

   fixed_height
      --  Height remains constant when layout changed.

      require
         valid: is_valid

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 CONTROL_WINDOW
   set_control (ctl: like control)
      --  Set associated control.

      require
         valid: ctl /= Void
      ensure
         keep_reference: ctl = control

feature(s) from PROGRESS_BAR
   --  Public interface

   set_position (p: DOUBLE)
      --  Set position of bar.

      require
         ratio_ok: p >= 0 and p <= 1

invariant
   has_parent: parent /= Void; --  hscroll: has_horizontal_scrollbar implies horizontal_scrollbar /= Void
 --  vscroll: has_horizontal_scrollbar implies vertical_scrollbar /= Void

end of PROGRESS_BAR