src/Tools/jEdit/src/jedit/OptionPane.scala

--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Sat Jun 27 00:19:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Tue Jun 30 21:22:50 2009 +0200
@@ -41,7 +41,7 @@
     if (Isabelle.Int_Property("font-size") != size)
     {
       Isabelle.Int_Property("font-size") = size
-      Swing.later { Isabelle.plugin.set_font(size) }
+      Swing_Thread.later { Isabelle.plugin.set_font(size) }
     }
   }
 }