+
Point of view
All features
deferred class GL_WIDGET
- not has_been_init implies opengl_widget.is_null
- has_been_init implies opengl_widget.is_not_null
- width >= min_width or computing_size
- height >= min_height or computing_size
- std_width > 0
- std_height > 0
- not x_shrink_allowed implies width >= std_width or computing_size
- not x_expand_allowed implies width <= std_width or computing_size
- not y_shrink_allowed implies height >= std_height or computing_size
- not y_expand_allowed implies height <= std_height or computing_size
require
- w >= min_width
- h >= min_height
ensure
require
- x >= 0
- y >= 0
- w >= min_width
- h >= min_height
ensure
ensure
-
good_hash_value: Result >= 0
basic_opengl_swap_buffers (ogl_widget:
POINTER)
basic_opengl_window_destroy (ogl_widget:
POINTER)
require
- p = Void implies parent /= Void
- p /= Void implies parent = Void
- p /= Void implies p.has_child(Current)
ensure
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective function
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
is_equal (other: GL_WIDGET):
BOOLEAN
deferred function
require
ensure
- Result implies hash_code = other.hash_code
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
deep_sky_blue_color:
COLOR
once function
light_sky_blue_color:
COLOR
once function
light_steel_blue_color:
COLOR
once function
pale_turquoise_color:
COLOR
once function
dark_turquoise_color:
COLOR
once function
medium_turquoise_color:
COLOR
once function
yellow_green_color:
COLOR
once function
light_yellow_color:
COLOR
once function
light_salmon_color:
COLOR
once function
pale_violet_red_color:
COLOR
once function
medium_violet_red_color:
COLOR
once function
dark_magenta_color:
COLOR
once function
medium_purple_color:
COLOR
once function