class interface HI

creation
   make
      --  Make application main window.

      ensure
         no_return:  --  warning: no return before app end

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 APPLICATION
   --  Application wide settings

   set_background_color (bcol: BRUSH)
      --  Set background window's colour brush 
      --  (for ALL windows in this application, it is not 
      --  processed immediately on opened windows).

      require
         valid_brush: bcol /= Void;
         valid_window: is_valid

   accept_dropped_files
      --  Accept files dropped onto our application window.

      require
         valid_window: is_valid

   set_icon (ico: ICON)
      --  Set window's icon (for ALL windows in this application).

      require
         valid_icon: ico /= Void;
         valid_window: is_valid

invariant
   is_unique:  --  only one instance of APPLICATION should exist per application

end of HI