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