equal
deleted
inserted
replaced
56 } |
56 } |
57 |
57 |
58 |
58 |
59 /* delayed events */ |
59 /* delayed events */ |
60 |
60 |
61 def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay = |
61 def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay = |
62 Standard_Thread.delay_first(delay) { later { event } } |
62 Isabelle_Thread.delay_first(delay) { later { event } } |
63 |
63 |
64 def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay = |
64 def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay = |
65 Standard_Thread.delay_last(delay) { later { event } } |
65 Isabelle_Thread.delay_last(delay) { later { event } } |
66 } |
66 } |