71704
|
1 |
/* Title: Pure/Concurrent/delay.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Delayed events.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
75393
|
10 |
object Delay {
|
71704
|
11 |
// delayed event after first invocation
|
|
12 |
def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
|
|
13 |
new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
|
|
14 |
|
|
15 |
// delayed event after last invocation
|
|
16 |
def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
|
|
17 |
new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
|
|
18 |
}
|
|
19 |
|
75393
|
20 |
final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit) {
|
71704
|
21 |
private var running: Option[Event_Timer.Request] = None
|
|
22 |
|
75393
|
23 |
private def run: Unit = {
|
71704
|
24 |
val do_run = synchronized {
|
|
25 |
if (running.isDefined) { running = None; true } else false
|
|
26 |
}
|
|
27 |
if (do_run) {
|
|
28 |
try { event }
|
|
29 |
catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
|
|
30 |
}
|
|
31 |
}
|
|
32 |
|
75380
|
33 |
def invoke(): Unit = synchronized {
|
71704
|
34 |
val new_run =
|
|
35 |
running match {
|
73367
|
36 |
case Some(request) => if (first) false else { request.cancel(); true }
|
71704
|
37 |
case None => true
|
|
38 |
}
|
|
39 |
if (new_run)
|
|
40 |
running = Some(Event_Timer.request(Time.now() + delay)(run))
|
|
41 |
}
|
|
42 |
|
75380
|
43 |
def revoke(): Unit = synchronized {
|
71704
|
44 |
running match {
|
73367
|
45 |
case Some(request) => request.cancel(); running = None
|
71704
|
46 |
case None =>
|
|
47 |
}
|
|
48 |
}
|
|
49 |
|
75380
|
50 |
def postpone(alt_delay: Time): Unit = synchronized {
|
71704
|
51 |
running match {
|
|
52 |
case Some(request) =>
|
|
53 |
val alt_time = Time.now() + alt_delay
|
73367
|
54 |
if (request.time < alt_time && request.cancel()) {
|
71704
|
55 |
running = Some(Event_Timer.request(alt_time)(run))
|
|
56 |
}
|
|
57 |
case None =>
|
|
58 |
}
|
|
59 |
}
|
|
60 |
}
|