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