# HG changeset patch
# User wenzelm
# Date 1246741397 -7200
# Node ID 3f0cee99b29f35dfb9eec3a9c68f1a8713935d8e
# Parent  6fce475ba1c6c92d0365bdf8e5a38adcc65211ff
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?);

diff -r 6fce475ba1c6 -r 3f0cee99b29f src/Tools/jEdit/src/jedit/TheoryView.scala
--- 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()
       }
     }
   }