# HG changeset patch
# User wenzelm
# Date 1649425773 -7200
# Node ID 6e0a452dab7212d7e4cf491ceafda91c8bf8c879
# Parent  2c861b196d522314f2be17f9d93ca44b6f8f075f
tuned signature -- avoid warnings for scala3;

diff -r 2c861b196d52 -r 6e0a452dab72 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Fri Apr 08 09:58:49 2022 +0200
+++ b/src/Tools/Graphview/popups.scala	Fri Apr 08 15:49:33 2022 +0200
@@ -30,25 +30,25 @@
       new Menu(caption) {
         contents +=
           new MenuItem(new Action("This") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false)))
           })
 
         contents +=
           new MenuItem(new Action("Family") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true)))
           })
 
         contents +=
           new MenuItem(new Action("Parents") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true)))
           })
 
         contents +=
           new MenuItem(new Action("Children") {
-            def apply =
+            def apply(): Unit =
               add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false)))
           })
 
@@ -77,7 +77,7 @@
                           contents +=
                             new MenuItem(
                               new Action(quote(to.toString)) {
-                                def apply =
+                                def apply(): Unit =
                                   add_mutator(
                                     Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                               })
@@ -96,7 +96,7 @@
                           contents +=
                             new MenuItem(
                               new Action(quote(from.toString)) {
-                                def apply =
+                                def apply(): Unit =
                                   add_mutator(
                                     Mutator.make(graphview, Mutator.Edge_Endpoints((from, to))))
                               })
@@ -113,7 +113,7 @@
 
     popup.add(
       new MenuItem(
-        new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer)
+        new Action("Remove all filters") { def apply(): Unit = graphview.model.Mutators(Nil) }).peer)
     popup.add(new JPopupMenu.Separator)
 
     if (mouse_node.isDefined) {
@@ -138,7 +138,7 @@
     }
 
     popup.add(new MenuItem(new Action("Fit to window") {
-      def apply = graph_panel.fit_to_window() }).peer
+      def apply(): Unit = graph_panel.fit_to_window() }).peer
     )
 
     popup