renamed Delay to clarified version Swing_Thread.delay;

--- 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);
 

--- 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()
       }
     }
   }