Merge pull request #207 from DecwLK/mouse_wheel_zoom

zooming now possible with ctrl+mousewheel

src/main/java/org/gecko/tools/Tool.java

@@ -2,6 +2,7 @@
 
 import javafx.event.Event;
 import javafx.event.EventHandler;
+import javafx.geometry.Point2D;
 import javafx.scene.Cursor;
 import javafx.scene.Node;
 import javafx.scene.input.MouseEvent;
@@ -20,6 +21,7 @@
 import org.gecko.view.views.viewelement.decorator.ConnectionElementScalerViewElementDecorator;
 import org.gecko.view.views.viewelement.decorator.ElementScalerViewElementDecorator;
 import org.gecko.view.views.viewelement.decorator.SelectableViewElementDecorator;
+import org.gecko.viewmodel.EditorViewModel;
 
 /**
  * An abstract representation of a tool used in the Gecko Graphic Editor, characterized by a {@link ToolType}. Follows
@@ -48,6 +50,16 @@ public void visitView(ViewElementPane pane) {
         pane.draw().setCursor(Cursor.DEFAULT);
         setAllHandlers(pane.draw(), null);
         setAllHandlers(pane.getWorld(), null);
+        pane.getWorld().setOnScroll(e -> {
+            if (!e.isControlDown() || e.getDeltaY() == 0) {
+                return;
+            }
+            e.consume();
+            double defaultZoomStep = EditorViewModel.getDefaultZoomStep();
+            double zoomFactor = e.getDeltaY() > 0 ? defaultZoomStep : 1 / defaultZoomStep;
+            Point2D pivot = pane.screenToWorldCoordinates(e.getScreenX(), e.getScreenY());
+            actionManager.run(actionManager.getActionFactory().createZoomAction(pivot, zoomFactor));
+        });
     }
 
     /**

src/main/java/org/gecko/tools/ZoomTool.java

@@ -4,12 +4,12 @@
 import javafx.scene.Cursor;
 import org.gecko.actions.ActionManager;
 import org.gecko.view.views.ViewElementPane;
+import org.gecko.viewmodel.EditorViewModel;
 
 /**
  * A concrete representation of a zoom-{@link Tool}, utilized for zooming in and out in the view.
  */
 public class ZoomTool extends Tool {
-    private static final double ZOOM_SCALE = 1.1;
 
     public ZoomTool(ActionManager actionManager) {
         super(actionManager, ToolType.ZOOM_TOOL, true);
@@ -24,9 +24,11 @@ public void visitView(ViewElementPane pane) {
             Point2D position = pane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
 
             if (event.isShiftDown()) {
-                actionManager.run(actionManager.getActionFactory().createZoomAction(position, 1 / ZOOM_SCALE));
+                actionManager.run(actionManager.getActionFactory()
+                    .createZoomAction(position, 1 / EditorViewModel.getDefaultZoomStep()));
             } else {
-                actionManager.run(actionManager.getActionFactory().createZoomAction(position, ZOOM_SCALE));
+                actionManager.run(
+                    actionManager.getActionFactory().createZoomAction(position, EditorViewModel.getDefaultZoomStep()));
             }
         });
     }

src/main/java/org/gecko/view/menubar/MenuBarBuilder.java

@@ -24,6 +24,7 @@
 import org.gecko.view.inspector.element.label.InspectorLabel;
 import org.gecko.view.inspector.element.textfield.InspectorRenameField;
 import org.gecko.view.views.shortcuts.Shortcuts;
+import org.gecko.viewmodel.EditorViewModel;
 import org.gecko.viewmodel.GeckoViewModel;
 import org.gecko.viewmodel.PositionableViewModelElement;
 import org.gecko.viewmodel.Renamable;
@@ -45,8 +46,6 @@ public class MenuBarBuilder {
     private final GeckoView view;
     private final ActionManager actionManager;
 
-    private static final double ZOOM_SCALE = 1.1;
-
     public MenuBarBuilder(GeckoView view, ActionManager actionManager) {
         this.view = view;
         this.actionManager = actionManager;
@@ -215,13 +214,13 @@ private Menu setupViewMenu() {
         // Zooming commands:
 
         MenuItem zoomInMenuItem = new MenuItem(ResourceHandler.getString("Buttons", "zoom_in"));
-        zoomInMenuItem.setOnAction(
-            e -> actionManager.run(actionManager.getActionFactory().createZoomCenterAction(ZOOM_SCALE)));
+        zoomInMenuItem.setOnAction(e -> actionManager.run(
+            actionManager.getActionFactory().createZoomCenterAction(EditorViewModel.getDefaultZoomStep())));
         zoomInMenuItem.setAccelerator(Shortcuts.ZOOM_IN.get());
 
         MenuItem zoomOutMenuItem = new MenuItem(ResourceHandler.getString("Buttons", "zoom_out"));
-        zoomOutMenuItem.setOnAction(
-            e -> actionManager.run(actionManager.getActionFactory().createZoomCenterAction(1 / ZOOM_SCALE)));
+        zoomOutMenuItem.setOnAction(e -> actionManager.run(
+            actionManager.getActionFactory().createZoomCenterAction(1 / EditorViewModel.getDefaultZoomStep())));
         zoomOutMenuItem.setAccelerator(Shortcuts.ZOOM_OUT.get());
 
         SeparatorMenuItem zoomToAppearanceSeparator = new SeparatorMenuItem();

src/main/java/org/gecko/view/views/FloatingUIBuilder.java

@@ -24,8 +24,6 @@
  */
 public class FloatingUIBuilder {
 
-    private static final double ZOOM_SCALE = 1.1;
-
     private static final int DEFAULT_BUTTON_SIZE = 30;
     private static final String FLOATING_BUTTON_STYLE_CLASS = "floating-ui-button";
     private static final String ZOOM_IN_STYLE_CLASS = "floating-zoom-in-button";
@@ -48,7 +46,8 @@ public Node buildZoomButtons() {
         Button zoomInButton = createStyledButton();
         zoomInButton.getStyleClass().add(ZOOM_IN_STYLE_CLASS);
         zoomInButton.setOnAction(event -> {
-            actionManager.run(actionManager.getActionFactory().createZoomCenterAction(ZOOM_SCALE));
+            actionManager.run(
+                actionManager.getActionFactory().createZoomCenterAction(EditorViewModel.getDefaultZoomStep()));
         });
         String zoomInTooltip = "%s (%s)".formatted(ResourceHandler.getString("Tooltips", "zoom_in"),
             Shortcuts.ZOOM_IN.get().getDisplayText());
@@ -62,8 +61,8 @@ public Node buildZoomButtons() {
 
         Button zoomOutButton = createStyledButton();
         zoomOutButton.getStyleClass().add(ZOOM_OUT_STYLE_CLASS);
-        zoomOutButton.setOnAction(
-            event -> actionManager.run(actionManager.getActionFactory().createZoomCenterAction(1 / ZOOM_SCALE)));
+        zoomOutButton.setOnAction(event -> actionManager.run(
+            actionManager.getActionFactory().createZoomCenterAction(1 / EditorViewModel.getDefaultZoomStep())));
         String zoomOutTooltip = "%s (%s)".formatted(ResourceHandler.getString("Tooltips", "zoom_out"),
             Shortcuts.ZOOM_OUT.get().getDisplayText());
         zoomOutButton.setTooltip(new Tooltip(zoomOutTooltip));

src/main/java/org/gecko/view/views/shortcuts/ShortcutHandler.java

@@ -11,6 +11,7 @@
 import org.gecko.actions.ActionManager;
 import org.gecko.tools.ToolType;
 import org.gecko.view.views.EditorView;
+import org.gecko.viewmodel.EditorViewModel;
 
 /**
  * An abstract representation of a handler for shortcut events, implementing the {@link EventHandler} interface, which
@@ -19,7 +20,6 @@
  * allow for actions to be run by using keyboard shortcuts.
  */
 public abstract class ShortcutHandler implements EventHandler<KeyEvent> {
-    private static final double ZOOM_FACTOR = 1.1;
     protected HashMap<KeyCodeCombination, Runnable> shortcuts = new HashMap<>();
     protected ActionManager actionManager;
     protected ActionFactory actionFactory;
@@ -65,10 +65,10 @@ private void addSelectStandardToolShortcuts() {
 
     private void addZoomShortcuts() {
         shortcuts.put(Shortcuts.ZOOM_IN.get(), () -> {
-            actionManager.run(actionFactory.createZoomCenterAction(ZOOM_FACTOR));
+            actionManager.run(actionFactory.createZoomCenterAction(EditorViewModel.getDefaultZoomStep()));
         });
         shortcuts.put(Shortcuts.ZOOM_OUT.get(), () -> {
-            actionManager.run(actionFactory.createZoomCenterAction(1 / ZOOM_FACTOR));
+            actionManager.run(actionFactory.createZoomCenterAction(1 / EditorViewModel.getDefaultZoomStep()));
         });
     }
 

src/main/java/org/gecko/viewmodel/EditorViewModel.java

@@ -48,6 +48,7 @@ public class EditorViewModel {
     private static final double MAX_ZOOM_SCALE = 2.5;
     private static final double MIN_ZOOM_SCALE = 0.1;
     private static final double DEFAULT_ZOOM_SCALE = 1;
+    private static final double DEFAULT_ZOOM_STEP = 1.1;
     private final int id;
     private final ActionManager actionManager;
     private final SystemViewModel currentSystem;
@@ -60,7 +61,6 @@ public class EditorViewModel {
     private final DoubleProperty zoomScaleProperty;
     private final BooleanProperty needsRefocusProperty;
 
-
     private final Property<Tool> currentToolProperty;
     private final Property<PositionableViewModelElement<?>> focusedElementProperty;
     private final boolean isAutomatonEditor;
@@ -260,6 +260,10 @@ public double getZoomScale() {
         return zoomScaleProperty.get();
     }
 
+    public static double getDefaultZoomStep() {
+        return DEFAULT_ZOOM_STEP;
+    }
+
     public void zoom(double factor, Point2D pivot) {
         if (factor < 0) {
             throw new IllegalArgumentException("Zoom factor must be positive");