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