class CHECK_SPACE

All features

This class is only for inserting the space needed to draw a check box. TODO: Should be created by renderer.

Direct parents

conformant parents

WIDGET

Summary

creation features

exported features

Details

default_create

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

default_create

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

min_width: INTEGER
min_height: INTEGER
std_width: INTEGER
std_height: INTEGER
width: INTEGER
height: INTEGER
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.

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

require

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

ensure

  • width = w
  • height = h

resize (w: INTEGER, h: INTEGER)

require

  • w >= min_width
  • h >= min_height

ensure

  • width = w
  • height = h

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
area: RECT
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

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

computing_size: BOOLEAN
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
state_normal: INTEGER
state_active: INTEGER
state_prelight: INTEGER
state_selected: INTEGER
state_insensitive: INTEGER

Class invariant