src/Pure/GUI/gui.scala

   Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
   JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{ComboBox, ScrollPane, TextArea}
-import scala.swing.event.SelectionChanged
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 
 object GUI {
   /* Swing look-and-feel */
 

         java_message.toArray.asInstanceOf[Array[AnyRef]], title,
           option_type, JOptionPane.QUESTION_MESSAGE)
     }
 
 
-  /* variations on ComboBox */
+  /* basic GUI components */
+
+  class Bool(label: String, init: Boolean = false) extends CheckBox(label) {
+    def clicked(state: Boolean): Unit = {}
+    def clicked(): Unit = {}
+
+    selected = init
+    reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
+  }
 
   class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
     def changed(): Unit = {}
 
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed() }
   }
+
+
+  /* zoom factor */
 
   private val Zoom_Factor = "([0-9]+)%?".r
 
   class Zoom extends Selector[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")