class interface F_EVENT creation make (name: STRING) -- Create event object or open existing. -- Default: new event is not set. require ok: name /= Void and then is_valid_name(name) ensure done: -- is_valid set make_anonymous -- Create event object with no name. -- Default: new event is not set. ensure done: is_valid make_auto (name: STRING) -- Create event object which is automatically reset after -- a single waiting thread has been released. -- Default: new event is not set. require ok: name /= Void and then is_valid_name(name) ensure done: -- is_valid set make_existing (name: STRING) -- Open existing event object. require ok: name /= Void and then is_valid_name(name) ensure done: -- is_valid set feature(s) from MEMORY -- Removal : dispose -- Object has been finalised. full_collect -- Force a full collection cycle if garbage collection is -- enabled; do nothing otherwise. feature(s) from F_SYNCH_OBJECT -- Notifier notifier: SYNCH_NOTIFIER -- Synchronisation notifier. feature(s) from F_SYNCH_OBJECT -- Status is_valid: BOOLEAN -- Is this object valid? is_valid_name (nm: STRING): BOOLEAN -- Is this string a valid event object name? require ok: nm /= Void ensure done: -- Result = (0 < nm.count < MAX_PATH and all nm.item /= '\') feature(s) from F_SYNCH_OBJECT synch_wait -- Synchronous wait for event. require valid: is_valid finite_wait (delay_ms: INTEGER) -- Synchronous wait for event during given delay. require ok: delay_ms >= 0; valid: is_valid wait -- Asynchronous non-blocking wait. require valid: is_valid close -- Close event object. require valid: is_valid ensure done: not is_valid feature(s) from F_SYNCH_OBJECT -- Command(s) set_command (cmd: GUI_COMMAND) -- Associate command with this event. require may_be_void: -- Void to cancel existing command ensure keep_reference: command = cmd feature(s) from F_EVENT -- Change status set -- Set event. require valid: is_valid reset -- Reset event. require valid: is_valid end of F_EVENT