class interface STD_SCROLLBAR

creation
   make_horizontal (par: WINDOW)

   make_vertical (par: WINDOW)
      require
         valid: par /= Void

feature(s) from CONTROL
   --  Implementation

   self: CHILD_WINDOW
      --  Associated child window.


feature(s) from CONTROL
   --  Dialog box

   has_dialog_box: BOOLEAN
      --  Check if control has associated dialog box.


   dialog_box: DIALOG
      --  Associated dialog which holds the control.

      require
         has_dialog: has_dialog_box
      ensure
         valid: Result /= Void

feature(s) from CONTROL
   --  Control's font

   set_font (ft: FONT)
      --  Set control font.

      require
         valid_font: ft /= Void

feature(s) from CONTROL
   --  Position, independent

   indep_size: RECTANGLE
      --  Control size using dialog coordinates.

      ensure
         is_copy:  --  can be modified.

   indep_set_size (sz: RECTANGLE)
      --  Set control size using dialog coordinates.

      require
         valid: sz /= Void
      ensure
         done: sz.is_equal(indep_size)

feature(s) from DIALOG_ELEMENT
   --  Device independent positioning

   indep_set_point (p: POINT)
      --  Set upper-left point of element using device independent units.

      require
         valid_point: p /= Void

   indep_set_width (wi: INTEGER)
      --  Set element's width using device independent units.

      require
         valid: wi >= 0

   indep_set_height (he: INTEGER)
      --  Set element's height using device independent units.

      require
         valid: he >= 0

feature(s) from DIALOG_ELEMENT
   --  Relative positioning

   place_right (other: DIALOG_ELEMENT)
      --  Place the current element to the right of other.

      require
         valid_other: other /= Void

   place_left (other: DIALOG_ELEMENT)
      --  Place the current element to the left of other.

      require
         valid_other: other /= Void

   place_above (other: DIALOG_ELEMENT)
      --  Place the current element above other.

      require
         valid_other: other /= Void

   place_under (other: DIALOG_ELEMENT)
      --  Place the current element under other.

      require
         valid_other: other /= Void

   place_just_under (other: DIALOG_ELEMENT)
      --  Place the current element exactly under 'other'.


   same_width (other: DIALOG_ELEMENT)
      --  Set the current element width to other's.

      require
         valid_other: other /= Void

   same_height (other: DIALOG_ELEMENT)
      --  Set the current element height to be the same as other's.

      require
         valid_other: other /= Void

   align_left (other: DIALOG_ELEMENT)
      --  Align left side of this element with the 
      --  left side of other.

      require
         ok: other /= Void

   align_right (other: DIALOG_ELEMENT)
      --  Align the right side of this element with the right 
      --  side of other.

      require
         ok: other /= Void

   align_top (other: DIALOG_ELEMENT)
      --  Align the top of this element with top of other.

      require
         ok: other /= Void

   align_bottom (other: DIALOG_ELEMENT)
      --  Align the bottom of this element with bottom of other.

      require
         ok: other /= Void

feature(s) from SCROLLBAR
   --  Type of scrollbar

   is_horizontal: BOOLEAN
      --  Is this scrollbar 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

feature(s) from STD_SCROLLBAR
   --  Default size

   default_height: INTEGER
      --  Default heigth of a control.


invariant
   valid_dir: is_horizontal xor is_vertical;

end of STD_SCROLLBAR