class interface F_SEMAPHORE creation make (nm: STRING; max_count: INTEGER) -- Create semaphore or open existing. -- Default: semaphore count is max_count. require ok: nm /= Void and then not is_valid_name(nm); ok_count: max_count > 0 ensure done: -- is_valid set make_existing (nm: STRING) -- Open existing semaphore. require ok: nm /= Void and then not is_valid_name(nm) 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_SEMAPHORE -- State release -- Release one semaphore slot. end of F_SEMAPHORE