--- a/src/Pure/GUI/gui_thread.scala Sat Sep 19 19:40:09 2015 +0200
+++ b/src/Pure/GUI/gui_thread.scala Sat Sep 19 20:31:57 2015 +0200
@@ -49,9 +49,9 @@
/* delayed events */
- def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
- Simple_Thread.delay_first(delay) { later { event } }
+ def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
+ : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
- def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
- Simple_Thread.delay_last(delay) { later { event } }
+ def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
+ : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
}