# HG changeset patch
# User wenzelm
# Date 1274390368 -7200
# Node ID 39f4cce5a22cef40b3109fdd73b2c2e0c5d3a93d
# Parent  cf66250122822320d058f0d876536fbf990c36aa
added somewhat generic zoom box;

diff -r cf6625012282 -r 39f4cce5a22c src/Pure/library.scala
--- 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) =