src/Tools/Graphview/src/popups.scala
changeset 50475 8cc351df4a23
parent 50472 bad1a1ca61e1
child 55618 995162143ef4
--- a/src/Tools/Graphview/src/popups.scala	Tue Dec 11 12:17:20 2012 +0100
+++ b/src/Tools/Graphview/src/popups.scala	Tue Dec 11 21:05:38 2012 +0100
@@ -18,10 +18,10 @@
   def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
     : JPopupMenu =
   {
-    val parameters = panel.visualizer.parameters
+    val visualizer = panel.visualizer
 
-    val add_mutator = panel.visualizer.model.Mutators.add _
-    val curr = panel.visualizer.model.current
+    val add_mutator = visualizer.model.Mutators.add _
+    val curr = visualizer.model.current
 
     def filter_context(ls: List[String], reverse: Boolean,
                        caption: String, edges: Boolean) =
@@ -29,7 +29,7 @@
         contents += new MenuItem(new Action("This") {
             def apply =
               add_mutator(
-                Mutators.create(parameters,
+                Mutators.create(visualizer,
                   Node_List(ls, reverse, false, false)
                 )
               )
@@ -38,7 +38,7 @@
         contents += new MenuItem(new Action("Family") {
             def apply =
               add_mutator(
-                Mutators.create(parameters,
+                Mutators.create(visualizer,
                   Node_List(ls, reverse, true, true)
                 )
               )
@@ -47,7 +47,7 @@
         contents += new MenuItem(new Action("Parents") {
             def apply =
               add_mutator(
-                Mutators.create(parameters,
+                Mutators.create(visualizer,
                   Node_List(ls, reverse, false, true)
                 )
               )
@@ -56,7 +56,7 @@
         contents += new MenuItem(new Action("Children") {
             def apply =
               add_mutator(
-                Mutators.create(parameters,
+                Mutators.create(visualizer,
                   Node_List(ls, reverse, true, false)
                 )
               )
@@ -89,7 +89,7 @@
                       contents += new MenuItem(new Action(to) {
                         def apply =
                           add_mutator(
-                            Mutators.create(parameters, Edge_Endpoints(from, to))
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
                           )
                       })
                     })
@@ -115,7 +115,7 @@
                       contents += new MenuItem(new Action(from) {
                         def apply =
                           add_mutator(
-                            Mutators.create(parameters, Edge_Endpoints(from, to))
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
                           )
                       })
                     })
@@ -130,14 +130,14 @@
     val popup = new JPopupMenu()
 
     popup.add(new MenuItem(new Action("Remove all filters") {
-          def apply = panel.visualizer.model.Mutators(Nil)
+          def apply = visualizer.model.Mutators(Nil)
         }).peer
     )
     popup.add(new JPopupMenu.Separator)
 
     if (under_mouse.isDefined) {
       val v = under_mouse.get
-      popup.add(new MenuItem("Mouseover: %s".format(panel.visualizer.Caption(v))) {
+      popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) {
         enabled = false
       }.peer)
 
@@ -151,7 +151,7 @@
         if (selected.length > 1) {
           "Multiple"
         } else {
-          panel.visualizer.Caption(selected.head)
+          visualizer.Caption(selected.head)
         }
       }