1.1 --- a/src/Pure/library.scala	Thu May 20 21:32:48 2010 +0200
     1.2 +++ b/src/Pure/library.scala	Thu May 20 23:19:28 2010 +0200
     1.3 @@ -11,6 +11,10 @@
     1.4  import javax.swing.JOptionPane
     1.5  
     1.6  
     1.7 +import scala.swing.ComboBox
     1.8 +import scala.swing.event.SelectionChanged
     1.9 +
    1.10 +
    1.11  object Library
    1.12  {
    1.13    /* separate */
    1.14 @@ -88,6 +92,31 @@
    1.15    def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
    1.16  
    1.17  
    1.18 +  /* zoom box */
    1.19 +
    1.20 +  def zoom_box(apply_factor: Int => Unit) =
    1.21 +    new ComboBox(
    1.22 +      List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
    1.23 +      val Factor = "([0-9]+)%?"r
    1.24 +      def reset(): Int = { selection.index = 3; 100 }
    1.25 +
    1.26 +      reactions += {
    1.27 +        case SelectionChanged(_) =>
    1.28 +          val factor =
    1.29 +            selection.item match {
    1.30 +              case Factor(s) =>
    1.31 +                val i = Integer.parseInt(s)
    1.32 +                if (10 <= i && i <= 1000) i else reset()
    1.33 +              case _ => reset()
    1.34 +            }
    1.35 +          apply_factor(factor)
    1.36 +        }
    1.37 +      reset()
    1.38 +      listenTo(selection)
    1.39 +      makeEditable()
    1.40 +    }
    1.41 +
    1.42 +
    1.43    /* timing */
    1.44  
    1.45    def timeit[A](message: String)(e: => A) =