class interface WIN_SPEC

creation
   make
      --  Smalleiffel


feature(s) from WINDOW
   --  Window public attributes

   parent: OVERLAPPED_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, in screen coordinates 
      --  for an overlapped window.

      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 OVERLAPPED_WINDOW
   --  Actions: iconisation.

   maximize
      --  Maximise (show full screen) the window.

      require
         valid: is_valid
      ensure
         not_iconic: is_iconic = false

   minimize
      --  Minimise (reduce to an icon) the window.

      require
         valid: is_valid
      ensure
         iconic: is_iconic

   restore
      --  Show the window and restore to its normal size if
      --  previously minimised or maximised.

      require
         valid: is_valid

feature(s) from OVERLAPPED_WINDOW
   --  Keyboard accelerators

   apply_accelerators
      --  Apply keyboard accelerators for items of menus CURRENTLY 
      --  associated with this window, it should be called after the 
      --  menu system has been set up to enable keyboard shortcuts.
      --  WARNING: If the menus are updated (or at least items with 
      --  associated accelerators are added or removed), this procedure 
      --  should be called again to update the table maintained by 
      --  the system.

      require
         valid: is_valid

feature(s) from DIALOG
   --  Default dialog font used by all controls

   set_font (ft: FONT)
      --  Set default font.

      require
         valid: ft /= Void
      ensure
         keep_reference: font = ft

feature(s) from DIALOG
   --  Action(s)

   apply
      --  Apply the dialog box settings.


   finish
      --  End processing.


feature(s) from DIALOG
   --  Buttons & keyboard interface

   set_ok_push_button (pushb: PUSH_BUTTON)
      --  Set the button which is a default push button at 
      --  initialisation or when no other button is active.
      --   will execute that button, which has to do 
      --  the actual action, such as calling 'apply' & 
      --  finish itself, like, for instance, OK_BUTTON.

      require
         ok: pushb /= Void
      ensure
         keep_reference: ok_push_button = pushb

   set_cancel_push_button (pushb: PUSH_BUTTON)
      --  Set the button which will be executed when  is 
      --  pressed. The button is responsible for closing the 
      --  dialog, without applying the settings. CANCEL_BUTTON 
      --  provides an implementation of such a button.

      require
         ok: pushb /= Void
      ensure
         keep_reference: cancel_push_button = pushb

feature(s) from MODELESS_DIALOG
   --  Creation

   dialog_make (p: like parent)
      --  Make dialog box with thick border.

      require
         valid: p /= Void

   make_thin (p: like parent)
      --  Make dialog box with thin border.

      require
         valid: p /= Void

feature(s) from MODELESS_DIALOG
   --  Other actions

   arrange
      --  Resize nicely so that the box is at the centre of the parent window 
      --  and encloses all controls.


feature(s) from WIN_SPEC
   --  Modal dialog implentation for type hole

   when_prepared
      --  Dialog is about to be displayed.


   when_applied
      --  Apply settings.


   when_finished
      --  Dialog has been closed.



end of WIN_SPEC