--- a/src/Pure/library.scala Thu May 20 21:32:48 2010 +0200
+++ b/src/Pure/library.scala Thu May 20 23:19:28 2010 +0200
@@ -11,6 +11,10 @@
import javax.swing.JOptionPane
+import scala.swing.ComboBox
+import scala.swing.event.SelectionChanged
+
+
object Library
{
/* separate */
@@ -88,6 +92,31 @@
def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
+ /* zoom box */
+
+ def zoom_box(apply_factor: Int => Unit) =
+ new ComboBox(
+ List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
+ val Factor = "([0-9]+)%?"r
+ def reset(): Int = { selection.index = 3; 100 }
+
+ reactions += {
+ case SelectionChanged(_) =>
+ val factor =
+ selection.item match {
+ case Factor(s) =>
+ val i = Integer.parseInt(s)
+ if (10 <= i && i <= 1000) i else reset()
+ case _ => reset()
+ }
+ apply_factor(factor)
+ }
+ reset()
+ listenTo(selection)
+ makeEditable()
+ }
+
+
/* timing */
def timeit[A](message: String)(e: => A) =