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