1/*  Title:      Pure/GUI/wrap_panel.scala
2    Author:     Makarius
3
4Panel with improved FlowLayout for wrapping of components over
5multiple lines, see also
6https://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
7scala.swing.FlowPanel.
8*/
9
10package isabelle
11
12
13import java.awt.{FlowLayout, Container, Dimension}
14import javax.swing.{JComponent, JPanel, JScrollPane}
15
16import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
17
18
19object Wrap_Panel
20{
21  val Alignment = FlowPanel.Alignment
22
23  class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
24    extends FlowLayout(align: Int, hgap: Int, vgap: Int)
25  {
26    override def preferredLayoutSize(target: Container): Dimension =
27      layout_size(target, true)
28
29    override def minimumLayoutSize(target: Container): Dimension =
30    {
31      val minimum = layout_size(target, false)
32      minimum.width -= (getHgap + 1)
33      minimum
34    }
35
36    private def layout_size(target: Container, preferred: Boolean): Dimension =
37    {
38      target.getTreeLock.synchronized
39      {
40        val target_width =
41          if (target.getSize.width == 0) Integer.MAX_VALUE
42          else target.getSize.width
43
44        val hgap = getHgap
45        val vgap = getVgap
46        val insets = target.getInsets
47        val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
48        val max_width = target_width - horizontal_insets_and_gap
49
50
51        /* fit components into rows */
52
53        val dim = new Dimension(0, 0)
54        var row_width = 0
55        var row_height = 0
56        def add_row()
57        {
58          dim.width = dim.width max row_width
59          if (dim.height > 0) dim.height += vgap
60          dim.height += row_height
61        }
62
63        for {
64          i <- (0 until target.getComponentCount).iterator
65          m = target.getComponent(i)
66          if m.isVisible
67          d = if (preferred) m.getPreferredSize else m.getMinimumSize()
68        }
69        {
70          if (row_width + d.width > max_width) {
71            add_row()
72            row_width = 0
73            row_height = 0
74          }
75
76          if (row_width != 0) row_width += hgap
77
78          row_width += d.width
79          row_height = row_height max d.height
80        }
81        add_row()
82
83        dim.width += horizontal_insets_and_gap
84        dim.height += insets.top + insets.bottom + vgap * 2
85
86
87        /* special treatment for ScrollPane */
88
89        val scroll_pane =
90          GUI.ancestors(target).exists(
91            {
92              case _: JScrollPane => true
93              case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
94              case _ => false
95            })
96        if (scroll_pane && target.isValid)
97          dim.width -= (hgap + 1)
98
99        dim
100      }
101    }
102  }
103
104  def apply(contents: List[Component] = Nil,
105      alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
106    new Wrap_Panel(contents, alignment)
107}
108
109class Wrap_Panel(contents0: List[Component] = Nil,
110    alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
111  extends Panel with SequentialContainer.Wrapper
112{
113  override lazy val peer: JPanel =
114    new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
115
116  contents ++= contents0
117
118  private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
119
120  def vGap: Int = layoutManager.getVgap
121  def vGap_=(n: Int) { layoutManager.setVgap(n) }
122  def hGap: Int = layoutManager.getHgap
123  def hGap_=(n: Int) { layoutManager.setHgap(n) }
124}
125