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