Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

em.network.multiplayer

Class EM_NET_OBJECT_ID_MANAGER



Creation

Features

Invariants

indexing

description

Manager for unique object IDs.

date

$Date: 2005/10/24 12:56:52 $

revision

$Revision: 1.15 $

class

EM_NET_OBJECT_ID_MANAGER

create

make

-- Initialize a new object id manager.

feature -- Access

set_unique_id_for_object (an_object: EM_NET_OBJECT)

-- Set a unique ID for an_object.

feature -- Commands

put (an_id: INTEGER)

-- Mark an_id as free for further use.

invariant

invariant_clause: True

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end