teal-src/util/timer.d.tl
changeset 12983 fbbf4f0db8f0
parent 12982 088d278c75b5
child 12984 6ebad8e16b3b
equal deleted inserted replaced
12982:088d278c75b5 12983:fbbf4f0db8f0
     1 local record util_timer
       
     2 	record task end
       
     3 	type timer_callback = function (number) : number
       
     4 	add_task : function ( number, timer_callback, any ) : task
       
     5 	stop : function ( task )
       
     6 	reschedule : function ( task, number ) : task
       
     7 end
       
     8 return util_timer