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) =