# HG changeset patch
# User wenzelm
# Date 1233090836 -3600
# Node ID bc22e49358f8411db158a5c87ab9c05f830b08cc
# Parent  87f4f70d61bb4058dd297c65c606a50ad09d7fb5
use plain toInt;

diff -r 87f4f70d61bb -r bc22e49358f8 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Tue Jan 27 19:52:56 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Tue Jan 27 22:13:56 2009 +0100
@@ -44,7 +44,7 @@
     addComponent(Isabelle.Property("font-size.title"), {
       try {
         if (Isabelle.Property("font-size") != null)
-          fontSize.setValue(Integer.valueOf(Isabelle.Property("font-size")))
+          fontSize.setValue(Isabelle.Property("font-size").toInt)
       }
       catch {
         case e : NumberFormatException =>