src/Pure/GUI/gui_thread.scala
changeset 61194 e4699ef5cf90
parent 57613 4c6d44a3a079
child 61556 0d4ee4168e41
equal deleted inserted replaced
61193:dde5ecbd5e10 61194:e4699ef5cf90
    47   }
    47   }
    48 
    48 
    49 
    49 
    50   /* delayed events */
    50   /* delayed events */
    51 
    51 
    52   def delay_first(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    52   def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
    53     Simple_Thread.delay_first(delay) { later { event } }
    53     : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
    54 
    54 
    55   def delay_last(delay: => Time)(event: => Unit): Simple_Thread.Delay =
    55   def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
    56     Simple_Thread.delay_last(delay) { later { event } }
    56     : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
    57 }
    57 }