author | wenzelm |
Thu, 14 Aug 2014 16:20:14 +0200 | |
changeset 57942 | e5bec882fdd0 |
parent 56356 | c3dbaa155ece |
child 60033 | 9a1d40876e9f |
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 |
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 { |
56356
c3dbaa155ece
tuned for-comprehensions -- less structure mapping;
wenzelm
parents:
53853
diff
changeset
|
65 |
i <- (0 until target.getComponentCount).iterator |
53711
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 |
} |