class interface MOUSE_CURSOR creation make_void -- Create cursor object (for current cursor manipulation). ensure not_valid: not is_valid make_resource (name: STRING) -- Load cursor from resource. require valid_name: name /= Void make_arrow -- Make standard arrow cursor. make_cross make_i_beam make_no make_up_arrow make_wait make_app_starting make_size_north_south make_size_west_east make_size_nw_se make_size_ne_sw feature(s) from MEMORY -- Removal : dispose full_collect -- Force a full collection cycle if garbage collection is -- enabled; do nothing otherwise. feature(s) from MOUSE_CURSOR -- Status is_valid: BOOLEAN feature(s) from MOUSE_CURSOR -- Current mouse cursor. apply -- Set current cursor to be this one (valid -- until next mouse movement). require valid_cursor: is_valid show_cursor -- Show current mouse cursor. hide_cursor -- Hide current mouse cursor. end of MOUSE_CURSOR