note description: "A mode (width, height, refresh rate, etc.) of a GAME_DISPLAY (screen)" author: "Louis Marchand" date: "Thu, 02 Apr 2015 02:40:10 +0000" revision: "2.0" class interface GAME_DISPLAY_MODE create make, make_with_refresh_rate create {GAME_SDL_ANY} own_from_pointer, shared_from_pointer feature -- Access width: INTEGER_32 assign set_width -- The width of Current require pointer_exists: exists ensure display_mode_width_not_changed: width = old width display_mode_height_not_changed: height = old height display_mode_refresh_rate_not_changed: refresh_rate = old refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format set_width (a_width: INTEGER_32) -- Assign width with the value of a_width. require pointer_exists: exists ensure display_mode_width_changed: width = a_width display_mode_height_not_changed: height = old height display_mode_refresh_rate_not_changed: refresh_rate = old refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format height: INTEGER_32 assign set_height -- The height of `Current require pointer_exists: exists ensure display_mode_width_not_changed: width = old width display_mode_height_not_changed: height = old height display_mode_refresh_rate_not_changed: refresh_rate = old refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format set_height (a_height: INTEGER_32) -- Assign height with the value of a_height. require pointer_exists: exists ensure display_mode_width_not_changed: width = old width display_mode_height_changed: height = a_height display_mode_refresh_rate_not_changed: refresh_rate = old refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format refresh_rate: INTEGER_32 assign set_refresh_rate -- The frame_rate of Current require pointer_exists: exists ensure display_mode_width_not_changed: width = old width display_mode_height_not_changed: height = old height display_mode_refresh_rate_not_changed: refresh_rate = old refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format set_refresh_rate (a_refresh_rate: INTEGER_32) -- Assign refresh_rate with the value of a_refresh_rate. require pointer_exists: exists ensure display_mode_width_not_changed: width = old width display_mode_height_not_changed: height = old height display_mode_refresh_rate_changed: refresh_rate = a_refresh_rate display_mode_pixel_format_not_changed: pixel_format ~ old pixel_format pixel_format: GAME_PIXEL_FORMAT_READABLE assign set_pixel_format -- The internal format of the pixel representation in memory. require pointer_exists: exists set_pixel_format (a_pixel_format: like pixel_format) -- Assign the pixel_format of the pixel representation in memory to the value of a_pixel_format. require pointer_exists: exists out: STRING_8 -- New string containing terse printable representation -- of current object require else pointer_exists: exists is_equal (a_other: like Current): BOOLEAN -- Is other attached to an object considered -- equal to current object? require else pointer_exists: exists feature -- Implementation structure_size: INTEGER_32 -- Size to allocate (in bytes). end -- class GAME_DISPLAY_MODE
Generated by ISE EiffelStudio