--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Jul 04 20:28:57 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Jul 04 22:25:47 2009 +0200
@@ -25,7 +25,7 @@
private val WIDTH = 10
private val HILITE_HEIGHT = 2
- val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
+ val repaint_delay = Delay(100){ repaint() }
setRequestFocusEnabled(false);
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Jul 04 20:28:57 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Jul 04 22:25:47 2009 +0200
@@ -95,15 +95,15 @@
/* painting */
- val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
+ val repaint_delay = Delay(100){ repaint_all() }
val change_receiver = actor {
loop {
react {
case _ => { // FIXME potentially blocking within loop/react!?!?!?!
Swing_Thread.now {
- repaint_delay.delay_or_ignore()
- phase_overview.repaint_delay.delay_or_ignore()
+ repaint_delay.prod()
+ phase_overview.repaint_delay.prod()
}
}
}
--- a/src/Tools/jEdit/src/utils/Delay.scala Sat Jul 04 20:28:57 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-/*
- * Delayed actions
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.utils
-
-import javax.swing.Timer
-import java.awt.event.{ActionListener, ActionEvent}
-
-class Delay(amount : Int, action : () => Unit) {
-
- val timer : Timer = new Timer(amount, new ActionListener {
- override def actionPerformed(e:ActionEvent) {
- action()
- }
- })
- // if called very often, action is executed at most once
- // in amount milliseconds
- def delay_or_ignore() = {
- if (!timer.isRunning()) {
- timer.setRepeats(false)
- timer.start()
- }
- }
-}