class interface CHILD_WINDOW

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

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

   make_child_scroll (par: like parent)
      --  Make a child window with both vertical and horizontal scrollbar.

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

   make_child_vertical_scroll (par: like parent)
      --  Make a child window with a vertical scrollbar.

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

   make_child_horizontal_scroll (par: like parent)
      --  Make a child window with a horizontal scrollbar.

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

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

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

end of CHILD_WINDOW