54 ExecutionContext.fromExecutorService(pool) |
54 ExecutionContext.fromExecutorService(pool) |
55 |
55 |
56 |
56 |
57 /* delayed events */ |
57 /* delayed events */ |
58 |
58 |
59 final class Delay private [Standard_Thread]( |
59 final class Delay private [Standard_Thread](first: Boolean, delay: => Time, event: => Unit) |
60 first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit) |
|
61 { |
60 { |
62 private var running: Option[Event_Timer.Request] = None |
61 private var running: Option[Event_Timer.Request] = None |
63 |
62 |
64 private def run: Unit = |
63 private def run: Unit = |
65 { |
64 { |
71 |
70 |
72 def invoke(): Unit = synchronized |
71 def invoke(): Unit = synchronized |
73 { |
72 { |
74 val new_run = |
73 val new_run = |
75 running match { |
74 running match { |
76 case Some(request) => if (first) false else { request.cancel; cancel(); true } |
75 case Some(request) => if (first) false else { request.cancel; true } |
77 case None => cancel(); true |
76 case None => true |
78 } |
77 } |
79 if (new_run) |
78 if (new_run) |
80 running = Some(Event_Timer.request(Time.now() + delay)(run)) |
79 running = Some(Event_Timer.request(Time.now() + delay)(run)) |
81 } |
80 } |
82 |
81 |
83 def revoke(): Unit = synchronized |
82 def revoke(): Unit = synchronized |
84 { |
83 { |
85 running match { |
84 running match { |
86 case Some(request) => request.cancel; cancel(); running = None |
85 case Some(request) => request.cancel; running = None |
87 case None => cancel() |
86 case None => |
88 } |
87 } |
89 } |
88 } |
90 |
89 |
91 def postpone(alt_delay: Time): Unit = synchronized |
90 def postpone(alt_delay: Time): Unit = synchronized |
92 { |
91 { |
93 running match { |
92 running match { |
94 case Some(request) => |
93 case Some(request) => |
95 val alt_time = Time.now() + alt_delay |
94 val alt_time = Time.now() + alt_delay |
96 if (request.time < alt_time && request.cancel) { |
95 if (request.time < alt_time && request.cancel) { |
97 cancel() |
|
98 running = Some(Event_Timer.request(alt_time)(run)) |
96 running = Some(Event_Timer.request(alt_time)(run)) |
99 } |
97 } |
100 else cancel() |
98 case None => |
101 case None => cancel() |
|
102 } |
99 } |
103 } |
100 } |
104 } |
101 } |
105 |
102 |
106 // delayed event after first invocation |
103 // delayed event after first invocation |
107 def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay = |
104 def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event) |
108 new Delay(true, delay, cancel, event) |
|
109 |
105 |
110 // delayed event after last invocation |
106 // delayed event after last invocation |
111 def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay = |
107 def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event) |
112 new Delay(false, delay, cancel, event) |
|
113 } |
108 } |