src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Sat Aug 13 11:59:06 2022 +0200
+++ b/src/Tools/Graphview/graph_panel.scala	Sat Aug 13 12:32:38 2022 +0200
@@ -298,7 +298,7 @@
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
-  private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) }
+  private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }