tuned;
authorwenzelm
Sun, 11 Jan 2009 22:02:27 +0100
changeset 34474 5f078db3cfc5
parent 34473 ed22ea317108
child 34475 f963335dbc6b
tuned;
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]