change_receiver: removed redundant Swing_Thread wrapper -- the Delay timer action is already in Swing;
added update_delay, which invokes token markup via buffer.propertiesChanged (potentially many other things?);

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jul 04 22:25:47 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Jul 04 23:03:17 2009 +0200
@@ -95,17 +95,16 @@
 
   /* painting */
 
+  val update_delay = Delay(500){ buffer.propertiesChanged() }
   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.prod()
-            phase_overview.repaint_delay.prod()
-          }
-        }
+        case _ =>
+          update_delay.prod()
+          repaint_delay.prod()
+          phase_overview.repaint_delay.prod()
       }
     }
   }