class interface WINDOW_SCROLLBAR

feature(s) from SCROLLBAR
   --  Type of scrollbar

   is_horizontal: BOOLEAN
      --  Is this scrollbar horizontal?

      ensure
         coherent: is_vertical = not is_horizontal

   is_vertical: BOOLEAN
      --  Is this scrollbar vertical?

      ensure
         coherent: is_vertical = not is_horizontal

feature(s) from SCROLLBAR
   --  Range & conversion from/to ratios

   Default_range: INTEGER

   range: INTEGER
      --  Slider position range.


   set_range (rg: INTEGER)
      --  Set slider position range.

      ensure
         ok:  --  range = rg unless recursive size change

   is_valid_range (r: INTEGER): BOOLEAN
      --  Is the given range valid?

      ensure
         done:  --  Result implies (r >= 1 and Result <= range)

   units_to_ratio (unit: INTEGER): DOUBLE
      --  Convert from 1-(INTEGER) to 0-1 (DOUBLE)

      require
         valid_range: is_valid_range(unit)
      ensure
         good_ratio: Result >= 0 and then Result <= 1

   ratio_to_units (ratio: DOUBLE): INTEGER
      --  Convert from 0-1 (DOUBLE) to 1-(INTEGER).

      require
         good_ratio: ratio >= 0 and then ratio <= 1
      ensure
         valid_range: is_valid_range(Result)

feature(s) from SCROLLBAR
   --  Steppings

   line_step: INTEGER
      --  Step to go when line up/down.


   page_step: INTEGER
      --  Step to go when page up/down.


   set_line_step (rg: INTEGER)
      --  Set line_step.

      require
         positive: rg >= 0

   set_page_step (rg: INTEGER)
      --  Set page_step.

      require
         positive: rg >= 0

feature(s) from SCROLLBAR
   --  Slider position and size

   slider_size: INTEGER
      --  Size of the slider. 


   set_slider_size (s: INTEGER)
      --  Set the size of the slider.

      require
         correct_size: is_valid_range(s)
      ensure
         size_set: slider_size = s

   slider_position: INTEGER
      --  Slider position range.

      ensure
         is_valid_range(Result)

   set_slider_position (pos: INTEGER)
      --  Set slider position range.

      require
         correct_pos: is_valid_range(pos)
      ensure
         pos_set: pos = slider_position

feature(s) from SCROLLBAR
   --  Event support

   tracked: BOOLEAN
      --  Is the mouse cursor currently moving slider


feature(s) from SCROLLBAR
   --  Command

   set_command (gc: GUI_COMMAND)
      --  Set when_slider_moved command.

      require
         nothing:  --  Void is no command

invariant
   valid_dir: is_horizontal xor is_vertical;

end of WINDOW_SCROLLBAR