try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
authorwenzelm
Thu, 20 May 2010 21:32:48 +0200
changeset 37017 cf6625012282
parent 37016 9dfcde68b383
child 37018 39f4cce5a22c
try CheckBox instead of ToggleButton, which is visually confusing without window focus, e.g. in a floating instance (problem of MacOS look-and-feel);
src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:10:03 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 21:32:48 2010 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 
-import scala.swing.{FlowPanel, Button, ToggleButton}
+import scala.swing.{FlowPanel, Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
 import javax.swing.JPanel
@@ -59,7 +59,7 @@
     reactions += { case ButtonClicked(_) => handle_update() }
   }
 
-  val follow = new ToggleButton("Follow")
+  val follow = new CheckBox("Follow")
   follow.selected = true