src/Tools/jEdit/src/jedit/OptionPane.scala
changeset 34751 6ed1b3701459
parent 34634 4b797391859a
     1.1 --- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Mon Dec 07 22:40:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Mon Dec 07 22:41:15 2009 +0100
     1.3 @@ -38,10 +38,6 @@
     1.4      Isabelle.Property("logic") = logic
     1.5  
     1.6      val size = font_size.getValue().asInstanceOf[Int]
     1.7 -    if (Isabelle.Int_Property("font-size") != size)
     1.8 -    {
     1.9 -      Isabelle.Int_Property("font-size") = size
    1.10 -      Swing_Thread.later { Isabelle.plugin.set_font(size) }
    1.11 -    }
    1.12 +    Isabelle.Int_Property("font-size") = size
    1.13    }
    1.14  }