# 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]