src/Tools/Graphview/popups.scala

 
 
 object Popups
 {
   def apply(
-    panel: Graph_Panel,
+    graph_panel: Graph_Panel,
     mouse_node: Option[Graph_Display.Node],
     selected_nodes: List[Graph_Display.Node]): JPopupMenu =
   {
-    val visualizer = panel.visualizer
+    val visualizer = graph_panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
     val visible_graph = visualizer.visible_graph
 
     def filter_context(

       popup.add(filter_context(selected_nodes, true, "Hide", true).peer)
       popup.add(filter_context(selected_nodes, false, "Show only", false).peer)
       popup.add(new JPopupMenu.Separator)
     }
 
-    popup.add(new MenuItem(new Action("Fit to window") { def apply = panel.fit_to_window() }).peer)
+    popup.add(new MenuItem(new Action("Fit to window") {
+      def apply = graph_panel.fit_to_window() }).peer
+    )
 
     popup
   }
 }