class interface F_TIMER

creation
   make
      --  Create timer.


feature(s) from F_TIMER
   --  Status

   is_active: BOOLEAN
      --  Is the timer active?


   set_delay (ms: INTEGER)
      --  Set the requested delay (in milliseconds) between executions 
      --  of this timer. This is a wish, actual delay between calls may 
      --  vary and can be greater or equal to 'delay'. This delay should 
      --  preferably not be too small (>100 ms).

      require
         down: not is_active
      ensure
         done: delay = ms

   set_command (com: GUI_COMMAND)
      --  Set callback command.

      require
         down: not is_active; --  void means no command
         void: 
      ensure
         done: command = com

   start
      --  Lauch the timer.

      require
         stopped: not is_active

   stop
      --  Stop the timer.

      require
         running: is_active


end of F_TIMER