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