diff -r f7c793b7fe7d -r 5d78bce4f5a4 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Tue May 06 11:16:13 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Tue May 06 15:54:22 2014 +0200
@@ -12,7 +12,8 @@
 import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JButton}
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
+  JButton, JTextField}
 
 import scala.collection.convert.WrapAsJava
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -124,7 +125,7 @@
       text match {
         case Factor(s) =>
           val i = Integer.parseInt(s)
-          if (10 <= i && i <= 1000) i else 100
+          if (10 <= i && i < 1000) i else 100
         case _ => 100
       }
 
@@ -138,12 +139,16 @@
     }
 
     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+    peer.getEditor.getEditorComponent match {
+      case text: JTextField => text.setColumns(3)
+      case _ =>
+    }
+
     reactions += {
       case SelectionChanged(_) => apply_factor(parse(selection.item))
     }
     listenTo(selection)
     selection.index = 3
-    prototypeDisplayValue = Some("00000%")
   }