class interface CARET

creation
   make (window: like parent; width, height: INTEGER)
      --  Create a caret.

      require
         valid_parent: window /= Void;
         good_size: width > 0 and height > 0;
         one_per_window: not has_caret(window)
      ensure
         created: is_valid = true;
         keep_reference: parent = window

feature(s) from CARET
   --  Preconditions

   has_caret (win: WINDOW): BOOLEAN
      --  Is there only one caret associated with the window?


   is_valid: BOOLEAN
      --  Is this caret valid?


feature(s) from CARET
   --  Actions

   hide
      --  Hide the caret.

      require
         valid: is_valid = true

   show
      --  Show caret.

      require
         valid: is_valid = true

   destroy
      --  Destroy caret, must be done before losing keyboard focus.

      require
         valid: is_valid = true
      ensure
         invalid: is_valid = false

feature(s) from CARET
   --  Position

   position: POINT
      --  Caret's current position.

      ensure
         is_copy:  --  may be modified.

   set_position (pt: POINT)
      --  Set caret's position in its parent window.

      require
         good_point: pt /= Void;
         valid: is_valid = true

invariant
   has_parent: parent /= Void;
   used_with_parent: is_valid implies parent.is_valid; -- used_when_focus: is_valid implies parent.has_focus (false when destroying)

end of CARET