--- a/src/Tools/jEdit/src/symbols_dockable.scala Sun Jan 18 17:31:27 2015 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sun Jan 18 17:32:38 2015 +0100
@@ -64,8 +64,8 @@
val search_page =
new TabbedPane.Page("search", new BorderPanel {
val results_panel = new Wrap_Panel
- add(search_field, BorderPanel.Position.North)
- add(new ScrollPane(results_panel), BorderPanel.Position.Center)
+ layout(search_field) = BorderPanel.Position.North
+ layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
val search_space =
(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList