src/Pure/GUI/gui.scala
changeset 56888 3e8cbb624cc5
parent 56874 5d78bce4f5a4
child 57044 042d6e58cb40
equal deleted inserted replaced
56887:1ca814da47ae 56888:3e8cbb624cc5
   138       }
   138       }
   139     }
   139     }
   140 
   140 
   141     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
   141     makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
   142     peer.getEditor.getEditorComponent match {
   142     peer.getEditor.getEditorComponent match {
   143       case text: JTextField => text.setColumns(3)
   143       case text: JTextField => text.setColumns(4)
   144       case _ =>
   144       case _ =>
   145     }
   145     }
   146 
   146 
   147     reactions += {
   147     reactions += {
   148       case SelectionChanged(_) => apply_factor(parse(selection.item))
   148       case SelectionChanged(_) => apply_factor(parse(selection.item))