src/Pure/library.scala
changeset 37048 d014976dd690
parent 37035 4834c3112788
child 37686 bb27d99a9a69
     1.1 --- a/src/Pure/library.scala	Fri May 21 22:08:13 2010 +0200
     1.2 +++ b/src/Pure/library.scala	Fri May 21 23:19:27 2010 +0200
     1.3 @@ -102,27 +102,27 @@
     1.4  
     1.5    /* zoom box */
     1.6  
     1.7 -  def zoom_box(apply_factor: Int => Unit) =
     1.8 -    new ComboBox(
     1.9 -      List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
    1.10 -      val Factor = "([0-9]+)%?"r
    1.11 -      def reset(): Int = { selection.index = 3; 100 }
    1.12 +  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
    1.13 +    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
    1.14 +  {
    1.15 +    val Factor = "([0-9]+)%?"r
    1.16 +    def parse(text: String): Int =
    1.17 +      text match {
    1.18 +        case Factor(s) =>
    1.19 +          val i = Integer.parseInt(s)
    1.20 +          if (10 <= i && i <= 1000) i else 100
    1.21 +        case _ => 100
    1.22 +      }
    1.23 +    def print(i: Int): String = i.toString + "%"
    1.24  
    1.25 -      reactions += {
    1.26 -        case SelectionChanged(_) =>
    1.27 -          val factor =
    1.28 -            selection.item match {
    1.29 -              case Factor(s) =>
    1.30 -                val i = Integer.parseInt(s)
    1.31 -                if (10 <= i && i <= 1000) i else reset()
    1.32 -              case _ => reset()
    1.33 -            }
    1.34 -          apply_factor(factor)
    1.35 -        }
    1.36 -      reset()
    1.37 -      listenTo(selection)
    1.38 -      makeEditable()
    1.39 +    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
    1.40 +    reactions += {
    1.41 +      case SelectionChanged(_) => apply_factor(parse(selection.item))
    1.42      }
    1.43 +    listenTo(selection)
    1.44 +    selection.index = 3
    1.45 +    prototypeDisplayValue = Some("00000%")
    1.46 +  }
    1.47  
    1.48  
    1.49    /* timing */