changeset 53853 | e8430d668f44 |
parent 53783 | f5e9d182f645 |
child 56356 | c3dbaa155ece |
53852:c7707223d782 | 53853:e8430d668f44 |
---|---|
1 /* Title: Pure/GUI/wrap_panel.scala |
1 /* Title: Pure/GUI/wrap_panel.scala |
2 Module: PIDE-GUI |
|
2 Author: Makarius |
3 Author: Makarius |
3 |
4 |
4 Panel with improved FlowLayout for wrapping of components over |
5 Panel with improved FlowLayout for wrapping of components over |
5 multiple lines, see also |
6 multiple lines, see also |
6 http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and |
7 http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and |