src/Pure/GUI/wrap_panel.scala
changeset 75393 87ebf5a50283
parent 75380 2cb2606ce075
child 78243 0e221a8128e4
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
    14 import javax.swing.{JComponent, JPanel, JScrollPane}
    14 import javax.swing.{JComponent, JPanel, JScrollPane}
    15 
    15 
    16 import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
    16 import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
    17 
    17 
    18 
    18 
    19 object Wrap_Panel
    19 object Wrap_Panel {
    20 {
       
    21   val Alignment = FlowPanel.Alignment
    20   val Alignment = FlowPanel.Alignment
    22 
    21 
    23   class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
    22   class Layout(align: Int = FlowLayout.CENTER, hgap: Int = 5, vgap: Int = 5)
    24     extends FlowLayout(align: Int, hgap: Int, vgap: Int)
    23       extends FlowLayout(align: Int, hgap: Int, vgap: Int) {
    25   {
       
    26     override def preferredLayoutSize(target: Container): Dimension =
    24     override def preferredLayoutSize(target: Container): Dimension =
    27       layout_size(target, true)
    25       layout_size(target, true)
    28 
    26 
    29     override def minimumLayoutSize(target: Container): Dimension =
    27     override def minimumLayoutSize(target: Container): Dimension = {
    30     {
       
    31       val minimum = layout_size(target, false)
    28       val minimum = layout_size(target, false)
    32       minimum.width -= (getHgap + 1)
    29       minimum.width -= (getHgap + 1)
    33       minimum
    30       minimum
    34     }
    31     }
    35 
    32 
    36     private def layout_size(target: Container, preferred: Boolean): Dimension =
    33     private def layout_size(target: Container, preferred: Boolean): Dimension = {
    37     {
       
    38       target.getTreeLock.synchronized {
    34       target.getTreeLock.synchronized {
    39         val target_width =
    35         val target_width =
    40           if (target.getSize.width == 0) Integer.MAX_VALUE
    36           if (target.getSize.width == 0) Integer.MAX_VALUE
    41           else target.getSize.width
    37           else target.getSize.width
    42 
    38 
    50         /* fit components into rows */
    46         /* fit components into rows */
    51 
    47 
    52         val dim = new Dimension(0, 0)
    48         val dim = new Dimension(0, 0)
    53         var row_width = 0
    49         var row_width = 0
    54         var row_height = 0
    50         var row_height = 0
    55         def add_row(): Unit =
    51         def add_row(): Unit = {
    56         {
       
    57           dim.width = dim.width max row_width
    52           dim.width = dim.width max row_width
    58           if (dim.height > 0) dim.height += vgap
    53           if (dim.height > 0) dim.height += vgap
    59           dim.height += row_height
    54           dim.height += row_height
    60         }
    55         }
    61 
    56 
    62         for {
    57         for {
    63           i <- (0 until target.getComponentCount).iterator
    58           i <- (0 until target.getComponentCount).iterator
    64           m = target.getComponent(i)
    59           m = target.getComponent(i)
    65           if m.isVisible
    60           if m.isVisible
    66           d = if (preferred) m.getPreferredSize else m.getMinimumSize()
    61           d = if (preferred) m.getPreferredSize else m.getMinimumSize()
    67         }
    62         } {
    68         {
       
    69           if (row_width + d.width > max_width) {
    63           if (row_width + d.width > max_width) {
    70             add_row()
    64             add_row()
    71             row_width = 0
    65             row_width = 0
    72             row_height = 0
    66             row_height = 0
    73           }
    67           }
   103   def apply(contents: List[Component] = Nil,
    97   def apply(contents: List[Component] = Nil,
   104       alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
    98       alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
   105     new Wrap_Panel(contents, alignment)
    99     new Wrap_Panel(contents, alignment)
   106 }
   100 }
   107 
   101 
   108 class Wrap_Panel(contents0: List[Component] = Nil,
   102 class Wrap_Panel(
   109     alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
   103   contents0: List[Component] = Nil,
   110   extends Panel with SequentialContainer.Wrapper
   104   alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
   111 {
   105 extends Panel with SequentialContainer.Wrapper {
   112   override lazy val peer: JPanel =
   106   override lazy val peer: JPanel =
   113     new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
   107     new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
   114 
   108 
   115   contents ++= contents0
   109   contents ++= contents0
   116 
   110