# HG changeset patch
# User wenzelm
# Date 1246739147 -7200
# Node ID 6fce475ba1c6c92d0365bdf8e5a38adcc65211ff
# Parent  c620d8c7f6b35fcdf6be5cdabe638f8e70eeabdc
replaced utils.Delay by tune version isabelle.Delay (Pure.jar);

diff -r c620d8c7f6b3 -r 6fce475ba1c6 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- 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);
 
diff -r c620d8c7f6b3 -r 6fce475ba1c6 src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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()
           }
         }
       }
diff -r c620d8c7f6b3 -r 6fce475ba1c6 src/Tools/jEdit/src/utils/Delay.scala
--- 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()
-    }
-  }
-}