src/Tools/Graphview/tree_panel.scala
changeset 66205 e9fa94f43a15
parent 60905 eba3acb72b55
child 66206 2d2082db735a
equal deleted inserted replaced
66204:b0a30a21f627 66205:e9fa94f43a15
   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()