# HG changeset patch
# User wenzelm
# Date 1246742784 -7200
# Node ID 3896caeedf8242846ce599624f9da431abf69703
# Parent  3f0cee99b29f35dfb9eec3a9c68f1a8713935d8e
renamed Delay to clarified version Swing_Thread.delay;

diff -r 3f0cee99b29f -r 3896caeedf82 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sat Jul 04 23:03:17 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sat Jul 04 23:26:24 2009 +0200
@@ -25,7 +25,7 @@
   private val WIDTH = 10
 	private val HILITE_HEIGHT = 2
 
-  val repaint_delay = Delay(100){ repaint() }
+  val repaint_delay = Swing_Thread.delay(100){ repaint() }
 
   setRequestFocusEnabled(false);
 
diff -r 3f0cee99b29f -r 3896caeedf82 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jul 04 23:03:17 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jul 04 23:26:24 2009 +0200
@@ -95,16 +95,16 @@
 
   /* painting */
 
-  val update_delay = Delay(500){ buffer.propertiesChanged() }
-  val repaint_delay = Delay(100){ repaint_all() }
+  val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() }
+  val repaint_delay = Swing_Thread.delay(100){ repaint_all() }
   
   val change_receiver = actor {
     loop {
       react {
         case _ =>
-          update_delay.prod()
-          repaint_delay.prod()
-          phase_overview.repaint_delay.prod()
+          update_delay()
+          repaint_delay()
+          phase_overview.repaint_delay()
       }
     }
   }