--- a/src/Tools/Graphview/tree_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
{
/* main actions */
- private def selection_action()
+ private def selection_action(): Unit =
{
if (tree != null) {
graphview.current_node = None
@@ -45,7 +45,7 @@
}
}
- private def point_action(path: TreePath)
+ private def point_action(path: TreePath): Unit =
{
if (tree_pane != null && path != null) {
val action_node =
@@ -131,11 +131,12 @@
if (ok) selection_field_foreground else graphview.error_color
}
- selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
- def changedUpdate(e: DocumentEvent) { selection_delay.invoke() }
- def insertUpdate(e: DocumentEvent) { selection_delay.invoke() }
- def removeUpdate(e: DocumentEvent) { selection_delay.invoke() }
- })
+ selection_field.peer.getDocument.addDocumentListener(
+ new DocumentListener {
+ def changedUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ def insertUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ def removeUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ })
private val selection_apply = new Button {
action = Action("<html><b>Apply</b></html>") { selection_action () }
@@ -148,7 +149,7 @@
/* main layout */
- def refresh()
+ def refresh(): Unit =
{
val new_nodes = graphview.visible_graph.topological_order
if (new_nodes != nodes) {