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