34407
|
1 |
/*
|
|
2 |
* Delayed actions
|
|
3 |
*
|
|
4 |
* @author Fabian Immler, TU Munich
|
|
5 |
*/
|
|
6 |
|
34405
|
7 |
package isabelle.utils
|
|
8 |
|
|
9 |
import javax.swing.Timer
|
|
10 |
import java.awt.event.{ActionListener, ActionEvent}
|
|
11 |
|
|
12 |
class Delay(amount : Int, action : () => Unit) {
|
|
13 |
|
|
14 |
val timer : Timer = new Timer(amount, new ActionListener {
|
34503
|
15 |
override def actionPerformed(e:ActionEvent) {
|
|
16 |
action()
|
34405
|
17 |
}
|
|
18 |
})
|
|
19 |
// if called very often, action is executed at most once
|
|
20 |
// in amount milliseconds
|
34503
|
21 |
def delay_or_ignore() = {
|
|
22 |
if (!timer.isRunning()) {
|
34405
|
23 |
timer.setRepeats(false)
|
|
24 |
timer.start()
|
|
25 |
}
|
|
26 |
}
|
|
27 |
}
|