indexing
description: "Objects that allow access to the OS clipboard."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
EV_CLIPBOARD
create
feature
data: ANY
EV_ANY
text: STRING
Result
require
not_destroyed: not is_destroyed
feature
remove_text
textVoid
require
not_destroyed: not is_destroyed
ensure
text_removed: text = void
set_text (a_text: STRING)
a_text
require
not_destroyed: not is_destroyed
a_text_not_void: a_text /= void
a_text_not_empty: not a_text.is_empty
ensure
text_cloned: text.is_equal (a_text) and then text /= a_text
feature
set_data (some_data: like data)
some_datadata
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
feature
copy (other: like Current)
other
EV_ANY
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
end -- EV_CLIPBOARD