--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/wrap_panel.scala Wed Sep 18 15:09:15 2013 +0200
@@ -0,0 +1,113 @@
+/* Title: Pure/System/wrap_panel.scala
+ Author: Makarius
+
+Panel with improved FlowLayout for wrapping of components over
+multiple lines, see also
+http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
+scala.swing.FlowPanel.
+*/
+
+package isabelle
+
+
+import java.awt.{FlowLayout, Container, Dimension}
+import javax.swing.{JPanel, JScrollPane, SwingUtilities}
+
+import scala.swing.{Panel, FlowPanel, Component, SequentialContainer}
+
+
+object Wrap_Panel
+{
+ val Alignment = FlowPanel.Alignment
+
+ class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
+ extends FlowLayout(align: Int, hgap: Int, vgap: Int)
+ {
+ override def preferredLayoutSize(target: Container): Dimension =
+ layout_size(target, true)
+
+ override def minimumLayoutSize(target: Container): Dimension =
+ {
+ val minimum = layout_size(target, false)
+ minimum.width -= (getHgap + 1)
+ minimum
+ }
+
+ private def layout_size(target: Container, preferred: Boolean): Dimension =
+ {
+ target.getTreeLock.synchronized
+ {
+ val target_width =
+ if (target.getSize.width == 0) Integer.MAX_VALUE
+ else target.getSize.width
+
+ val hgap = getHgap
+ val vgap = getVgap
+ val insets = target.getInsets
+ val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
+ val max_width = target_width - horizontal_insets_and_gap
+
+ val dim = new Dimension(0, 0)
+ var row_width = 0
+ var row_height = 0
+ def add_row()
+ {
+ dim.width = dim.width max row_width
+ if (dim.height > 0) dim.height += vgap
+ dim.height += row_height
+ }
+
+ for {
+ i <- 0 until target.getComponentCount
+ m = target.getComponent(i)
+ if m.isVisible
+ d = if (preferred) m.getPreferredSize else m.getMinimumSize()
+ }
+ {
+ if (row_width + d.width > max_width) {
+ add_row()
+ row_width = 0
+ row_height = 0
+ }
+
+ if (row_width != 0) row_width += hgap
+
+ row_width += d.width
+ row_height = row_height max d.height
+ }
+ add_row()
+
+ dim.width += horizontal_insets_and_gap
+ dim.height += insets.top + insets.bottom + vgap * 2
+
+ SwingUtilities.getAncestorOfClass(classOf[JScrollPane], target) match {
+ case scroll_pane: Container if target.isValid =>
+ dim.width -= (hgap + 1)
+ case _ =>
+ }
+
+ dim
+ }
+ }
+ }
+}
+
+
+class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*)
+ extends Panel with SequentialContainer.Wrapper
+{
+ override lazy val peer: JPanel =
+ new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
+
+ def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*)
+ def this() = this(Wrap_Panel.Alignment.Center)()
+
+ contents ++= contents0
+
+ private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
+
+ def vGap: Int = layoutManager.getVgap
+ def vGap_=(n: Int) { layoutManager.setVgap(n) }
+ def hGap: Int = layoutManager.getHgap
+ def hGap_=(n: Int) { layoutManager.setHgap(n) }
+}
--- a/src/Pure/build-jars Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Pure/build-jars Wed Sep 18 15:09:15 2013 +0200
@@ -65,6 +65,7 @@
System/system_channel.scala
System/system_dialog.scala
System/utf8.scala
+ System/wrap_panel.scala
Thy/html.scala
Thy/present.scala
Thy/thy_header.scala
--- a/src/Tools/jEdit/src/find_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, Component, TextField, CheckBox, Label, ComboBox}
+import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -154,7 +154,7 @@
}
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), context, limit, allow_dups,
process_indicator.component, apply_query, zoom)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button}
+import scala.swing.Button
import scala.swing.event.ButtonClicked
import java.lang.System
@@ -94,7 +94,7 @@
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, CheckBox}
+import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
import java.lang.System
@@ -155,6 +155,7 @@
}
}
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(auto_update, update, detach, zoom)
+ private val controls =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, Component, Label, TextField, CheckBox}
+import scala.swing.{Button, Component, Label, TextField, CheckBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
@@ -174,7 +174,7 @@
}
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
provers_label, Component.wrap(provers), isar_proofs,
process_indicator.component, apply_query, cancel_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 13:31:44 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 15:09:15 2013 +0200
@@ -10,7 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
+import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
@@ -83,7 +83,7 @@
private val logic = Isabelle_Logic.logic_selector(true)
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(continuous_checking, session_phase, logic)
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
add(controls.peer, BorderLayout.NORTH)
--- 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)