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