indexing
description: "Instance of an application."
status: "See notice at end of class."
date: "$Date$"
revision: "$Revision$"
class interface
WEL_INSTANCE
create
make (a_hinstance: POINTER)
a_hinstance
ensure
item_set: item = a_hinstance
feature
item: POINTER
WEL_ANY
name: STRING
ensure
result_not_void: Result /= void
result_not_empty: not Result.is_empty
feature
exists: BOOLEAN
item
WEL_ANY
ensure WEL_ANY
Result = (item /= default_pointer)
shared: BOOLEAN
item
item
destroy_item
item
WEL_ANY
feature
set_shared
shared
WEL_ANY
ensure WEL_ANY
shared: shared
set_unshared
shared
WEL_ANY
ensure WEL_ANY
unshared: not shared
feature
set_item (an_item: POINTER)
iteman_item
WEL_ANY
ensure WEL_ANY
item_set: item = an_item
feature
dispose
Current
Current
WEL_ANY
feature
to_integer: INTEGER
item
WEL_ANY
ensure WEL_ANY
Result = cwel_pointer_to_integer (item)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- WEL_INSTANCE