--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -10,7 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Label, ListView, Alignment, ScrollPane, Component, TextField}
+import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}
import java.lang.System
@@ -142,7 +142,8 @@
s match { case Properties.Value.Double(x) => x >= 0.0 case _ => false })
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(threshold_label, threshold_value)
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value)
add(controls.peer, BorderLayout.NORTH)