--- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 20:16:40 2017 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Jun 27 21:36:58 2017 +0200
@@ -122,7 +122,7 @@
private class Search_Panel extends BorderPanel {
val search_field = new TextField(10)
- val results_panel = new Wrap_Panel
+ val results_panel = Wrap_Panel()
layout(search_field) = BorderPanel.Position.North
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
@@ -155,12 +155,11 @@
pages ++=
Symbol.groups.map({ case (group, symbols) =>
+ val control = group == "control"
new TabbedPane.Page(group,
- new ScrollPane(new Wrap_Panel {
- val control = group == "control"
- contents ++= symbols.map(new Symbol_Component(_, control))
- if (control) contents += new Reset_Component
- }), null)
+ new ScrollPane(Wrap_Panel(
+ symbols.map(new Symbol_Component(_, control)) :::
+ (if (control) List(new Reset_Component) else Nil))), null)
})
val search_panel = new Search_Panel