# HG changeset patch
# User wenzelm
# Date 1379513378 -7200
# Node ID bb15972a644debec40270963601f77ccc69802f8
# Parent  ea51046be71b0c3ef42358cfb3d0b31a38c55d1b
improved layout, with special treatment for ScrollPane;

diff -r ea51046be71b -r bb15972a644d src/Pure/System/wrap_panel.scala
--- a/src/Pure/System/wrap_panel.scala	Wed Sep 18 15:50:59 2013 +0200
+++ b/src/Pure/System/wrap_panel.scala	Wed Sep 18 16:09:38 2013 +0200
@@ -11,9 +11,9 @@
 
 
 import java.awt.{FlowLayout, Container, Dimension}
-import javax.swing.{JPanel, JScrollPane, SwingUtilities}
+import javax.swing.{JComponent, JPanel, JScrollPane}
 
-import scala.swing.{Panel, FlowPanel, Component, SequentialContainer}
+import scala.swing.{Panel, FlowPanel, Component, SequentialContainer, ScrollPane}
 
 
 object Wrap_Panel
@@ -47,6 +47,9 @@
         val horizontal_insets_and_gap = insets.left + insets.right + (hgap * 2)
         val max_width = target_width - horizontal_insets_and_gap
 
+
+        /* fit components into rows */
+
         val dim = new Dimension(0, 0)
         var row_width = 0
         var row_height = 0
@@ -80,11 +83,18 @@
         dim.width += horizontal_insets_and_gap
         dim.height += insets.top + insets.bottom + vgap * 2
 
-        SwingUtilities.getAncestorOfClass(classOf[JScrollPane], target) match {
-          case scroll_pane: Container if target.isValid =>
-            dim.width -= (hgap + 1)
-          case _ =>
-        }
+
+        /* special treatment for ScrollPane */
+
+        val scroll_pane =
+          GUI.ancestors(target).exists(
+            {
+              case _: JScrollPane => true
+              case c: JComponent if Component.wrap(c).isInstanceOf[ScrollPane] => true
+              case _ => false
+            })
+        if (scroll_pane && target.isValid)
+          dim.width -= (hgap + 1)
 
         dim
       }
diff -r ea51046be71b -r bb15972a644d src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 18 15:50:59 2013 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 18 16:09:38 2013 +0200
@@ -12,7 +12,7 @@
 import java.awt.Font
 
 import scala.swing.event.ValueChanged
-import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
+import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
 
 import org.gjt.sp.jedit.View
 
@@ -60,16 +60,16 @@
     pages ++=
       Symbol.groups map { case (group, symbols) =>
         new TabbedPane.Page(group,
-          new FlowPanel {
+          new ScrollPane(new Wrap_Panel {
             contents ++= symbols.map(new Symbol_Component(_))
             if (group == "control") contents += new Reset_Component
-          }, null)
+          }), null)
       }
     pages += new TabbedPane.Page("search", new BorderPanel {
       val search = new TextField(10)
-      val results_panel = new FlowPanel
+      val results_panel = new Wrap_Panel
       add(search, BorderPanel.Position.North)
-      add(results_panel, BorderPanel.Position.Center)
+      add(new ScrollPane(results_panel), BorderPanel.Position.Center)
       listenTo(search)
       val delay_search =
         Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {