# HG changeset patch
# User wenzelm
# Date 1231707747 -3600
# Node ID 5f078db3cfc53b19f763c7ee6d9874d67c43f3ed
# Parent  ed22ea317108215619348094180cb9707c6c12c4
tuned;

diff -r ed22ea317108 -r 5f078db3cfc5 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Jan 11 21:52:40 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Jan 11 22:02:27 2009 +0100
@@ -10,10 +10,9 @@
 
 import java.awt.BorderLayout
 import java.awt.GridBagConstraints.HORIZONTAL
-import java.awt.BorderLayout.{ WEST, CENTER, EAST }
-import java.awt.event.{ ActionListener, ActionEvent }
-import javax.swing.{ JTextField, JButton, JPanel, JLabel, JFileChooser, 
-                     JSpinner, SwingUtilities, JComboBox }
+import java.awt.BorderLayout.{WEST, CENTER, EAST}
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{JTextField, JButton, JPanel, JLabel, JFileChooser, JSpinner, JComboBox}
 
 import org.gjt.sp.jedit.AbstractOptionPane
 
@@ -72,10 +71,7 @@
     if (Isabelle.Property("font-path") != name || Isabelle.Property("font-size") != size.toString) {
       Isabelle.Property("font-path") = name
       Isabelle.Property("font-size") = size.toString
-      SwingUtilities invokeLater new Runnable() {
-        override def run() = 
-          Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue)
-      }
+      Swing.later { Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue) }
     }
     
     val logic = logicName.getSelectedItem.asInstanceOf[String]