src/Pure/library.scala

--- a/src/Pure/library.scala	Wed Dec 12 13:28:23 2012 +0100
+++ b/src/Pure/library.scala	Wed Dec 12 14:54:48 2012 +0100
@@ -178,8 +178,16 @@
           if (10 <= i && i <= 1000) i else 100
         case _ => 100
       }
+
     def print(i: Int): String = i.toString + "%"
 
+    def set_item(i: Int) {
+      peer.getEditor match {
+        case null =>
+        case editor => editor.setItem(print(i))
+      }
+    }
+
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
     reactions += {
       case SelectionChanged(_) => apply_factor(parse(selection.item))