class interface APPLICATION creation 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 APPLICATION