equal
deleted
inserted
replaced
141 action = Action("<html><b>Apply</b></html>") { selection_action () } |
141 action = Action("<html><b>Apply</b></html>") { selection_action () } |
142 tooltip = "Apply tree selection to graph" |
142 tooltip = "Apply tree selection to graph" |
143 } |
143 } |
144 |
144 |
145 private val controls = |
145 private val controls = |
146 new Wrap_Panel(Wrap_Panel.Alignment.Right)(selection_label, selection_field, selection_apply) |
146 Wrap_Panel(List(selection_label, selection_field, selection_apply), |
|
147 Wrap_Panel.Alignment.Right) |
147 |
148 |
148 |
149 |
149 /* main layout */ |
150 /* main layout */ |
150 |
151 |
151 def refresh() |
152 def refresh() |