class interface F_SYNCH_OBJECT 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 end of F_SYNCH_OBJECT