author | wenzelm |
Sun, 28 Feb 2016 21:20:51 +0100 | |
changeset 62459 | 7a5d88dd8cc9 |
parent 60033 | 9a1d40876e9f |
child 66205 | e9fa94f43a15 |
permissions | -rw-r--r-- |
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 |
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
3 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
4 |
Panel with improved FlowLayout for wrapping of components over |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
5 |
multiple lines, see also |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
6 |
http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
7 |
scala.swing.FlowPanel. |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
8 |
*/ |
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 |
package isabelle |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
11 |
|
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 |
import java.awt.{FlowLayout, Container, Dimension} |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
14 |
import javax.swing.{JComponent, JPanel, JScrollPane} |
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
15 |
|
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
16 |
import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane} |
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
17 |
|
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 |
object Wrap_Panel |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
20 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
21 |
val Alignment = FlowPanel.Alignment |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
22 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
23 |
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
|
24 |
extends FlowLayout(align: Int, hgap: Int, vgap: Int) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
25 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
26 |
override def preferredLayoutSize(target: Container): Dimension = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
27 |
layout_size(target, true) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
28 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
29 |
override def minimumLayoutSize(target: Container): Dimension = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
30 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
31 |
val minimum = layout_size(target, false) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
32 |
minimum.width -= (getHgap + 1) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
33 |
minimum |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
34 |
} |
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 |
private def layout_size(target: Container, preferred: Boolean): Dimension = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
37 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
38 |
target.getTreeLock.synchronized |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
39 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
40 |
val target_width = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
41 |
if (target.getSize.width == 0) Integer.MAX_VALUE |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
42 |
else target.getSize.width |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
43 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
44 |
val hgap = getHgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
45 |
val vgap = getVgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
46 |
val insets = target.getInsets |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
47 |
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
|
48 |
val max_width = target_width - horizontal_insets_and_gap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
49 |
|
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
50 |
|
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
51 |
/* fit components into rows */ |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
52 |
|
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
53 |
val dim = new Dimension(0, 0) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
54 |
var row_width = 0 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
55 |
var row_height = 0 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
56 |
def add_row() |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
57 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
58 |
dim.width = dim.width max row_width |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
59 |
if (dim.height > 0) dim.height += vgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
60 |
dim.height += row_height |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
61 |
} |
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 |
for { |
56356
c3dbaa155ece
tuned for-comprehensions -- less structure mapping;
wenzelm
parents:
53853
diff
changeset
|
64 |
i <- (0 until target.getComponentCount).iterator |
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
65 |
m = target.getComponent(i) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
66 |
if m.isVisible |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
67 |
d = if (preferred) m.getPreferredSize else m.getMinimumSize() |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
68 |
} |
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 |
if (row_width + d.width > max_width) { |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
71 |
add_row() |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
72 |
row_width = 0 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
73 |
row_height = 0 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
74 |
} |
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 |
if (row_width != 0) row_width += hgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
77 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
78 |
row_width += d.width |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
79 |
row_height = row_height max d.height |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
80 |
} |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
81 |
add_row() |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
82 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
83 |
dim.width += horizontal_insets_and_gap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
84 |
dim.height += insets.top + insets.bottom + vgap * 2 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
85 |
|
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
86 |
|
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
87 |
/* special treatment for ScrollPane */ |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
88 |
|
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
89 |
val scroll_pane = |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
90 |
GUI.ancestors(target).exists( |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
91 |
{ |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
92 |
case _: JScrollPane => true |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
93 |
case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
94 |
case _ => false |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
95 |
}) |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
96 |
if (scroll_pane && target.isValid) |
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53711
diff
changeset
|
97 |
dim.width -= (hgap + 1) |
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
98 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
99 |
dim |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
100 |
} |
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 |
class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
107 |
extends Panel with SequentialContainer.Wrapper |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
108 |
{ |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
109 |
override lazy val peer: JPanel = |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
110 |
new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
111 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
112 |
def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*) |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
113 |
def this() = this(Wrap_Panel.Alignment.Center)() |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
114 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
115 |
contents ++= contents0 |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
116 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
117 |
private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout] |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
118 |
|
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
119 |
def vGap: Int = layoutManager.getVgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
120 |
def vGap_=(n: Int) { layoutManager.setVgap(n) } |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
121 |
def hGap: Int = layoutManager.getHgap |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
122 |
def hGap_=(n: Int) { layoutManager.setHgap(n) } |
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
diff
changeset
|
123 |
} |