src/Pure/General/swing_thread.scala
changeset 32501 41aa620885c2
parent 32494 4ab2292e452a
child 34026 0cb44ac299f8
equal deleted inserted replaced
32494:4ab2292e452a 32501:41aa620885c2
    34   }
    34   }
    35 
    35 
    36 
    36 
    37   /* delayed actions */
    37   /* delayed actions */
    38 
    38 
    39   // turn multiple invocations into single action within time span
    39   private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
    40   def delay(time_span: Int)(action: => Unit): () => Unit =
       
    41   {
    40   {
    42     val listener =
    41     val listener =
    43       new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
    42       new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
    44     val timer = new Timer(time_span, listener)
    43     val timer = new Timer(time_span, listener)
    45     def invoke()
    44     timer.setRepeats(false)
    46     {
    45 
    47       if (!timer.isRunning()) {
    46     def invoke() { if (first) timer.start() else timer.restart() }
    48         timer.setRepeats(false)
       
    49         timer.start()
       
    50       }
       
    51     }
       
    52     invoke _
    47     invoke _
    53   }
    48   }
       
    49 
       
    50   // delayed action after first invocation
       
    51   def delay_first = delayed_action(true) _
       
    52 
       
    53   // delayed action after last invocation
       
    54   def delay_last = delayed_action(false) _
    54 }
    55 }