class BUTTON

All features

Direct parents

conformant parents

GRAPHIC, SUB_WINDOW, WHEN_DOUBLE_CLICKED

non-conformant parents

WHEN_MIDDLE_CLICKED, WHEN_RIGHT_CLICKED

Known children

conformant children

REPEAT_BUTTON

Summary

creation features

exported features

Details

make (p: CONTAINER)
with_label (p: CONTAINER, text: UNICODE_STRING)
make_layout (p: CONTAINER, lo: LAYOUT)

require

  • p /= Void
  • lo /= Void
  • lo.container = Void

ensure

  • parent = p
  • layout = lo

sub_window_create (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER, parent_window: WINDOW)

require

  • x.in_range(0, parent_window.width - 1)
  • y.in_range(0, parent_window.height - 1)
  • w.in_range(1, parent_window.width - x)
  • h.in_range(1, parent_window.height - y)

default_create

Default creation method. It is used when no creation method is specified if allowed. Note it may be renamed.

make (p: CONTAINER)
with_label (p: CONTAINER, text: UNICODE_STRING)
layout: ROW_LAYOUT
set_state (n: INTEGER)
update_decoration
vision: VISION
font_manager: FONT_MANAGER
default_font: BASIC_FONT
white_color: COLOR
black_color: COLOR
dim_grey_color: COLOR
dark_grey_color: COLOR
grey_color: COLOR
light_grey_color: COLOR
dark_blue_color: COLOR
medium_blue_color: COLOR
blue_color: COLOR
royal_blue_color: COLOR
deep_sky_blue_color: COLOR
sky_blue_color: COLOR
light_sky_blue_color: COLOR
steel_blue_color: COLOR
light_steel_blue_color: COLOR
light_blue_color: COLOR
pale_turquoise_color: COLOR
dark_turquoise_color: COLOR
medium_turquoise_color: COLOR
turquoise_color: COLOR
dark_cyan_color: COLOR
cyan_color: COLOR
light_cyan_color: COLOR
dark_green_color: COLOR
green_color: COLOR
light_green_color: COLOR
yellow_green_color: COLOR
dark_khaki_color: COLOR
khaki_color: COLOR
yellow_color: COLOR
light_yellow_color: COLOR
gold_color: COLOR
beige_color: COLOR
chocolate_color: COLOR
firebrick_color: COLOR
brown_color: COLOR
dark_salmon_color: COLOR
salmon_color: COLOR
light_salmon_color: COLOR
dark_orange_color: COLOR
orange_color: COLOR
orange_red_color: COLOR
dark_red_color: COLOR
red_color: COLOR
hot_pink_color: COLOR
deep_pink_color: COLOR
pink_color: COLOR
light_pink_color: COLOR
pale_violet_red_color: COLOR
maroon_color: COLOR
medium_violet_red_color: COLOR
violet_red_color: COLOR
violet_color: COLOR
dark_magenta_color: COLOR
magenta_color: COLOR
dark_violet_color: COLOR
blue_violet_color: COLOR
medium_purple_color: COLOR
purple_color: COLOR
state_normal: INTEGER
state_active: INTEGER
state_prelight: INTEGER
state_selected: INTEGER
state_insensitive: INTEGER
center_alignment: ALIGNMENT
left_alignment: ALIGNMENT
right_alignment: ALIGNMENT
top_alignment: ALIGNMENT
down_alignment: ALIGNMENT
top_left_alignment: ALIGNMENT
top_right_alignment: ALIGNMENT
down_right_alignment: ALIGNMENT
down_left_alignment: ALIGNMENT
make_layout (p: CONTAINER, lo: LAYOUT)

require

  • p /= Void
  • lo /= Void
  • lo.container = Void

ensure

  • parent = p
  • layout = lo

sub_window_create (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER, parent_window: WINDOW)

require

  • x.in_range(0, parent_window.width - 1)
  • y.in_range(0, parent_window.height - 1)
  • w.in_range(1, parent_window.width - x)
  • h.in_range(1, parent_window.height - y)

default_init
set_parent (p: CONTAINER)

require

  • p = Void implies parent /= Void
  • p /= Void implies parent = Void
  • p /= Void implies p.has_child(Current)

ensure

  • parent = p

set_background_color (c: COLOR)

The color is copied, next changes to c won't change the background. Call clear_area (or refresh) to update the background from application, not needed from renderer

require

  • c /= Void

set_background_pixmap (p: PIXMAP)

Call this function again if you modify the pixmap (copy may have been done)

require

  • p /= Void

map
unmap
mapped: BOOLEAN

Warning: this information is asynchronous

expose_event
clear_without_expose

clear the all the drawable area. WARNING: don't redraw the content (no expose event)

area: RECT
refresh

clear and update entire object (sub_window(s) are not updated).

clear

clear and update entire object (sub_window(s) are not updated).

as_x_root (x: INTEGER): INTEGER

TODO: add basic conversion to speed up

require

  • x >= 0
  • x < width
  • x >= pos_x
  • x < pos_x + width

as_y_root (y: INTEGER): INTEGER

TODO: add basic conversion to speed up

require

  • y >= 0
  • y < height
  • y >= pos_y
  • y < pos_y + height

expose_paint

expose_paint paint with depth limited to the first window Containers have to propagate, with special attention to windows where expose_paint do nothing.

require

  • layout /= Void

set_geometry (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)

Position may be negative (used for scrolling).

require

  • w >= min_width
  • h >= min_height
  • x >= 0
  • y >= 0
  • w >= min_width
  • h >= min_height

ensure

  • width = w
  • height = h

set_requisition (min_w: INTEGER, min_h: INTEGER, std_w: INTEGER, std_h: INTEGER)

require

  • min_w.in_range(0, std_w)
  • min_h.in_range(0, std_h)

ensure

  • not layout_update_paused implies layout_ready or not done

adjust_size
resize (w: INTEGER, h: INTEGER)

Warning: do not redraw content if not window subtype

require

  • w >= min_width
  • h >= min_height

ensure

  • width = w
  • height = h

paint_decorations (x: INTEGER, y: INTEGER)
resize_decorations (w: INTEGER, h: INTEGER)
set_mapped (b: BOOLEAN)
geometry_changed (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)
dispatch

Should be called only from set_geometry and set_requisition.

require

  • not layout_ready
  • layout /= Void

ensure

  • layout_ready

basic_window_create (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER, parent_win: POINTER, decorate: BOOLEAN): POINTER
basic_window_set_geometry (win: POINTER, x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)
basic_window_set_position (win: POINTER, x: INTEGER, y: INTEGER)
basic_window_set_size (win: POINTER, x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)
basic_window_set_bg_color (win: POINTER, color: POINTER)
basic_window_set_bg_pixmap (win: POINTER, pixmap: POINTER)
basic_window_clear_no_expose (win: POINTER)
basic_window_set_kbd_focus (win: POINTER)
basic_window_map (win: POINTER)
basic_window_unmap (win: POINTER)
basic_window_get_drawing_widget (w: POINTER): POINTER
default_create

Default creation method. It is used when no creation method is specified if allowed. Note it may be renamed.

container_init
width: INTEGER
height: INTEGER
min_width: INTEGER
min_height: INTEGER
std_width: INTEGER
std_height: INTEGER
child: FAST_ARRAY[WIDGET]
layout_update_paused: BOOLEAN

TODO: suppress. Handle this with mapped

set_layout (l: LAYOUT)

Change the layout for the container (layout choose children position and size). The layout has to be free (not used by another container).

require

  • l /= Void
  • l.container = Void

ensure

  • layout = l
  • layout.container = Current
  • not layout_update_paused implies layout_ready

layout_pause

TODO: remove when mapped ready

require

  • not layout_update_paused

ensure

  • layout_update_paused

layout_continue

TODO: remove when mapped ready

require

  • layout_update_paused

ensure

  • layout_ready
  • not layout_update_paused

child_attach (w: WIDGET)

Add widget w in this container.

require

  • layout /= Void
  • w /= Void
  • w.parent = Void
  • not has_child(w)

ensure

  • w.parent = Current
  • has_child(w)
  • last_child = w
  • not layout_update_paused implies layout_ready or not done

    TODO: not mapped implies not layout_ready???

child_dettach (w: WIDGET)
This feature is obsolete: Use `child_detach' instead.
child_detach (w: WIDGET)

Remove widget w from this container.

require

  • w /= Void
  • has_child(w)

ensure

  • child.count = old child.count - 1
  • not has_child(w)
  • w.parent = Void
  • not layout_update_paused implies layout_ready

    TODO: not mapped implies not layout_ready???

has_child (w: WIDGET): BOOLEAN
last_child: WIDGET

require

  • not is_empty

is_empty: BOOLEAN
clear_area (x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)

clear area and emit expose event (contents will be drawn) x and y are relative to current object

require

  • w > 0
  • h > 0
  • area.include(x, y)
  • area.include(x + w - 1, y + h - 1)

done: BOOLEAN

TODO: suppress. Handle this with mapped

child_requisition_changed

require

  • layout /= Void

ensure

  • not layout_update_paused implies layout_ready or not done

layout_ready: BOOLEAN
requisition_changed: BOOLEAN
invalidate_layout

ensure

  • not layout_ready

computing_size: BOOLEAN

This is only used for invariant defined in widget. Sizes may be invalid while they are computed

basic_window_clear_area (window: POINTER, x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)

TODO: invalid for pixmap. Redefine allowed ?

basic_window_clear_area_no_expose (window: POINTER, x: INTEGER, y: INTEGER, w: INTEGER, h: INTEGER)

TODO: invalid for pixmap. Redefine allowed ?

drawing_widget: POINTER

Because Windows can not paint on widgets like windows or bitmaps, it needs another object (Device Context) attached to the widget. For X11, it is the same value as widget.

parent: CONTAINER
pos_x: INTEGER
pos_y: INTEGER
x_shrink_allowed: BOOLEAN
x_expand_allowed: BOOLEAN
y_shrink_allowed: BOOLEAN
y_expand_allowed: BOOLEAN
valid_width (w: INTEGER): BOOLEAN
valid_height (h: INTEGER): BOOLEAN
root_area: RECT
set_x_shrink (b: BOOLEAN)
set_x_expand (b: BOOLEAN)
set_y_shrink (b: BOOLEAN)
set_y_expand (b: BOOLEAN)
set_shrink (b: BOOLEAN)

change both x and y shrink state

set_expand (b: BOOLEAN)

change both x and y expand state

state: INTEGER

use values from STATE_CONSTANTS

frozen is_state_normal: BOOLEAN
frozen is_state_active: BOOLEAN
frozen is_state_prelight: BOOLEAN
frozen is_state_selected: BOOLEAN
frozen is_state_insensitive: BOOLEAN
frozen set_state_normal
frozen set_state_active
frozen set_state_prelight
frozen set_state_selected
frozen set_state_insensitive
set_state (n: INTEGER)
renderer: RENDERER
deferred hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

deferred is_equal (other: BUTTON): BOOLEAN

Is other attached to an object considered equal to current object ?

require

  • other /= Void

ensure

  • Result implies hash_code = other.hash_code
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

widget: POINTER

widget identifier from the native graphic API.

when_left_down (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_left_down_signal: SIGNAL_0
when_left_up (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_left_up_signal: SIGNAL_0
when_middle_down (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_middle_down_signal: SIGNAL_0
when_middle_up (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_middle_up_signal: SIGNAL_0
when_right_down (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_right_down_signal: SIGNAL_0
when_right_up (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_right_up_signal: SIGNAL_0
when_wheel_up (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_wheel_up_signal: SIGNAL_0
when_wheel_down (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_wheel_down_signal: SIGNAL_0
when_pointer_move (p: PROCEDURE [O_ -> TUPLE][TUPLE 2 [A_, B_][INTEGERINTEGER]])
when_pointer_move_signal: SIGNAL_2 [E, F][INTEGERINTEGER]
when_pointer_enter (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_pointer_enter_signal: SIGNAL_0
when_pointer_leave (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_pointer_leave_signal: SIGNAL_0
when_key_down (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_key_down_signal: SIGNAL_0
when_mapped (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_mapped_signal: SIGNAL_0
when_unmapped (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_unmapped_signal: SIGNAL_0
when_geometry_change (p: PROCEDURE [O_ -> TUPLE][TUPLE 4 [A_, B_, C_, D_][INTEGERINTEGERINTEGERINTEGER]])
when_geometry_change_signal: SIGNAL_4 [E, F, G, H][INTEGERINTEGERINTEGERINTEGER]
when_expose (p: PROCEDURE [O_ -> TUPLE][TUPLE])
when_expose_signal: SIGNAL_0
double_click_delay: INTEGER
double_click_signal: SIGNAL_0
when_double_clicked (p: PROCEDURE [O_ -> TUPLE][TUPLE])

double click on left button NOTE: click has been generated before!

set_double_click_delay (cd: INTEGER)

Set the maximum time (in milliseconds) between a up and next down sequence for a double-click to be emitted

require

  • cd > 0 and then cd < 1000

ensure

  • double_click_delay = cd

default_double_click_delay: INTEGER

Maximum time (milliseconds) for a up/nextdown sequence to be considered as double click

when_double_clicked_init
left_up_time: INTEGER
private_left_down

require

    ensure

    • left_is_down

    private_left_up

    require

    • left_is_down

    ensure

    • not left_is_down

    left_click_signal: SIGNAL_0
    when_left_clicked (p: PROCEDURE [O_ -> TUPLE][TUPLE])
    left_is_down: BOOLEAN
    left_may_click: BOOLEAN
    private_left_pointer_enter
    private_left_pointer_leave
    is_pointer_inside: BOOLEAN
    pointer_status_init
    private_pointer_in
    private_pointer_out
    pointer_status_initialized: BOOLEAN
    middle_click_signal: SIGNAL_0
    when_middle_clicked (p: PROCEDURE [O_ -> TUPLE][TUPLE])
    middle_is_down: BOOLEAN
    when_middle_clicked_init
    middle_may_click: BOOLEAN
    private_middle_down

    ensure

    • middle_is_down

    private_middle_up

    require

    • middle_is_down

    ensure

    • not middle_is_down

    private_middle_pointer_enter
    right_click_signal: SIGNAL_0
    when_right_clicked (p: PROCEDURE [O_ -> TUPLE][TUPLE])
    right_is_down: BOOLEAN
    when_right_clicked_init
    right_may_click: BOOLEAN
    private_right_down

    ensure

    • right_is_down

    private_right_up

    require

    • right_is_down

    ensure

    • not right_is_down

    private_right_pointer_enter

    Class invariant