src/Tools/jEdit/src/plugin.scala
changeset 43390 7ee98a3802af
parent 43282 5d294220ca43
child 43443 5d9693c2337e
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 15:58:01 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 14 17:24:23 2011 +0200
@@ -373,11 +373,7 @@
         }
 
       case msg: PropertiesChanged =>
-        Swing_Thread.now {
-          Isabelle.setup_tooltips()
-          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
-            Document_View(text_area).get.extend_styles()
-        }
+        Swing_Thread.now { Isabelle.setup_tooltips() }
         Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>