equal
deleted
inserted
replaced
21 |
21 |
22 class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel |
22 class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel |
23 { |
23 { |
24 /* main actions */ |
24 /* main actions */ |
25 |
25 |
26 private def selection_action() |
26 private def selection_action(): Unit = |
27 { |
27 { |
28 if (tree != null) { |
28 if (tree != null) { |
29 graphview.current_node = None |
29 graphview.current_node = None |
30 graphview.Selection.clear() |
30 graphview.Selection.clear() |
31 val paths = tree.getSelectionPaths |
31 val paths = tree.getSelectionPaths |
43 } |
43 } |
44 graph_panel.repaint() |
44 graph_panel.repaint() |
45 } |
45 } |
46 } |
46 } |
47 |
47 |
48 private def point_action(path: TreePath) |
48 private def point_action(path: TreePath): Unit = |
49 { |
49 { |
50 if (tree_pane != null && path != null) { |
50 if (tree_pane != null && path != null) { |
51 val action_node = |
51 val action_node = |
52 path.getLastPathComponent match { |
52 path.getLastPathComponent match { |
53 case tree_node: DefaultMutableTreeNode => |
53 case tree_node: DefaultMutableTreeNode => |
129 } |
129 } |
130 selection_field.foreground = |
130 selection_field.foreground = |
131 if (ok) selection_field_foreground else graphview.error_color |
131 if (ok) selection_field_foreground else graphview.error_color |
132 } |
132 } |
133 |
133 |
134 selection_field.peer.getDocument.addDocumentListener(new DocumentListener { |
134 selection_field.peer.getDocument.addDocumentListener( |
135 def changedUpdate(e: DocumentEvent) { selection_delay.invoke() } |
135 new DocumentListener { |
136 def insertUpdate(e: DocumentEvent) { selection_delay.invoke() } |
136 def changedUpdate(e: DocumentEvent): Unit = selection_delay.invoke() |
137 def removeUpdate(e: DocumentEvent) { selection_delay.invoke() } |
137 def insertUpdate(e: DocumentEvent): Unit = selection_delay.invoke() |
138 }) |
138 def removeUpdate(e: DocumentEvent): Unit = selection_delay.invoke() |
|
139 }) |
139 |
140 |
140 private val selection_apply = new Button { |
141 private val selection_apply = new Button { |
141 action = Action("<html><b>Apply</b></html>") { selection_action () } |
142 action = Action("<html><b>Apply</b></html>") { selection_action () } |
142 tooltip = "Apply tree selection to graph" |
143 tooltip = "Apply tree selection to graph" |
143 } |
144 } |
146 Wrap_Panel(List(selection_label, selection_field, selection_apply)) |
147 Wrap_Panel(List(selection_label, selection_field, selection_apply)) |
147 |
148 |
148 |
149 |
149 /* main layout */ |
150 /* main layout */ |
150 |
151 |
151 def refresh() |
152 def refresh(): Unit = |
152 { |
153 { |
153 val new_nodes = graphview.visible_graph.topological_order |
154 val new_nodes = graphview.visible_graph.topological_order |
154 if (new_nodes != nodes) { |
155 if (new_nodes != nodes) { |
155 tree.clearSelection |
156 tree.clearSelection |
156 |
157 |