fix region scaling; fix zoom at mouse cursor

DecwLK · Mar 7, 2024 · 6bb601f · 6bb601f
1 parent 58b481d
commit 6bb601f
Show file tree

Hide file tree

Showing 7 changed files with 34 additions and 30 deletions.
diff --git a/src/main/java/org/gecko/actions/MoveEdgeViewModelElementAction.java b/src/main/java/org/gecko/actions/MoveEdgeViewModelElementAction.java
@@ -57,7 +57,7 @@ Action getUndoAction(ActionFactory actionFactory) {
     }
 
     private StateViewModel attemptRelocation() {
-        return getStateViewModelAt(elementScalerBlock.getPosition().add(delta));
+        return getStateViewModelAt(elementScalerBlock.getLayoutPosition().add(delta));
     }
 
     private StateViewModel getStateViewModelAt(Point2D point) {

diff --git a/src/main/java/org/gecko/actions/MoveSystemConnectionViewModelElementAction.java b/src/main/java/org/gecko/actions/MoveSystemConnectionViewModelElementAction.java
@@ -112,7 +112,7 @@ private PortViewModel getPortViewModelAt() {
             return null;
         }
 
-        return getPortViewModelAt(elementScalerBlock.getPosition().add(delta));
+        return getPortViewModelAt(elementScalerBlock.getLayoutPosition().add(delta));
     }
 
     private PortViewModel getPortViewModelAt(Point2D point) {

diff --git a/src/main/java/org/gecko/tools/CursorTool.java b/src/main/java/org/gecko/tools/CursorTool.java
@@ -130,7 +130,7 @@ private void setBlockScalerElementHandlers(ElementScalerBlock scaler) {
             scaler.setDragging(true);
             oldPosition = scaler.getDecoratorTarget().getTarget().getPosition();
             oldSize = scaler.getDecoratorTarget().getTarget().getSize();
-            startDragPosition = scaler.localToParent(scaler.sceneToLocal(event.getSceneX(), event.getSceneY()));
+            startDragPosition = viewPane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
             previousDragPosition = startDragPosition;
             isDragging = true;
         });
@@ -139,7 +139,7 @@ private void setBlockScalerElementHandlers(ElementScalerBlock scaler) {
             if (!isDragging) {
                 return;
             }
-            Point2D newPosition = scaler.localToParent(scaler.sceneToLocal(event.getSceneX(), event.getSceneY()));
+            Point2D newPosition = viewPane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
 
             if (!scaler.setCenter(newPosition)) {
                 cancelDrag(scaler);
@@ -184,7 +184,7 @@ private void setConnectionScalerElementsHandlers(ElementScalerBlock scaler) {
             Point2D eventPosition =
                 viewPane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
             Point2D delta = eventPosition.subtract(previousDragPosition);
-            scaler.setPosition(scaler.getPosition().add(delta));
+            scaler.setLayoutPosition(scaler.getLayoutPosition().add(delta));
             previousDragPosition = eventPosition;
         });
         scaler.setOnMouseReleased(event -> {
@@ -193,7 +193,7 @@ private void setConnectionScalerElementsHandlers(ElementScalerBlock scaler) {
             }
             Point2D endWorldPos =
                 viewPane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
-            scaler.setPosition(scaler.getPosition().add(startDragPosition.subtract(endWorldPos)));
+            scaler.setLayoutPosition(scaler.getLayoutPosition().add(startDragPosition.subtract(endWorldPos)));
             Action moveAction;
 
             if (editorViewModel.isAutomatonEditor()) {

diff --git a/src/main/java/org/gecko/view/views/ViewElementPane.java b/src/main/java/org/gecko/view/views/ViewElementPane.java
@@ -96,7 +96,8 @@ public void addElement(ViewElement<?> element) {
     }
 
     public void removeElement(ViewElement<?> element) {
-        world.getChildren().remove(element.drawElement());
+        elements.remove(element);
+        orderChildren();
     }
 
     public ViewElement<?> findViewElement(PositionableViewModelElement<?> element) {
@@ -160,12 +161,12 @@ private void updateWorldSize(Point2D oldPivot) {
 
     private void updateWorldSize() {
         updateMinAndMaxWorldPosition();
-        double newMinX = Math.min(minWorldPosition.getX(), 0) - widthPadding.get();
-        double newMinY = Math.min(minWorldPosition.getY(), 0) - heightPadding.get();
-        double newMaxX = Math.max(maxWorldPosition.getX(), 0) + widthPadding.get();
-        double newMaxY = Math.max(maxWorldPosition.getY(), 0) + heightPadding.get();
-        double newWidth = newMaxX - newMinX;
-        double newHeight = newMaxY - newMinY;
+        Point2D localMin = worldTolocalCoordinates(minWorldPosition);
+        Point2D localMax = worldTolocalCoordinates(maxWorldPosition);
+        double newWidth =
+            Math.max(pane.getViewportBounds().getWidth(), localMax.getX() - localMin.getX() + widthPadding.get() * 2);
+        double newHeight =
+            Math.max(pane.getViewportBounds().getHeight(), localMax.getY() - localMin.getY() + heightPadding.get() * 2);
         world.setMinSize(newWidth, newHeight);
         pane.layout();
         updateOffset();
@@ -205,7 +206,7 @@ private void setupListeners() {
             }
         });
         evm.getZoomScaleProperty().addListener((obs, oldV, newV) -> {
-            updateWorldSize();
+            updateWorldSize(evm.getPivot());
         });
         pane.hvalueProperty().addListener((obs, oldH, newH) -> {
             evm.updatePivot(screenCenterWorldCoords());

diff --git a/src/main/java/org/gecko/view/views/viewelement/BlockViewElement.java b/src/main/java/org/gecko/view/views/viewelement/BlockViewElement.java
@@ -45,11 +45,12 @@ protected BlockViewElement(PositionableViewModelElement<? extends Element> posit
     }
 
     private void calculateEdgePoints(PositionableViewModelElement<?> target) {
+        Point2D position = target.getPosition();
         double width = target.getSize().getX();
         double height = target.getSize().getY();
-        edgePoints.get(0).setValue(new Point2D(0, 0));
-        edgePoints.get(1).setValue(new Point2D(width, 0));
-        edgePoints.get(2).setValue(new Point2D(width, height));
-        edgePoints.get(3).setValue(new Point2D(0, height));
+        edgePoints.get(0).setValue(position.add(new Point2D(0, 0)));
+        edgePoints.get(1).setValue(position.add(new Point2D(width, 0)));
+        edgePoints.get(2).setValue(position.add(new Point2D(width, height)));
+        edgePoints.get(3).setValue(position.add(new Point2D(0, height)));
     }
 }
diff --git a/src/main/java/org/gecko/view/views/viewelement/decorator/ElementScalerBlock.java b/src/main/java/org/gecko/view/views/viewelement/decorator/ElementScalerBlock.java
@@ -40,8 +40,7 @@ protected void refreshListeners() {
 
         ChangeListener<Point2D> newListener = (observable, oldValue, newValue) -> {
             if (!isDragging) {
-                setLayoutX(newValue.getX() - (getWidth() / 2));
-                setLayoutY(newValue.getY() - (getHeight() / 2));
+                updatePosition();
             }
         };
         decoratorTarget.getEdgePoints().get(index).addListener(newListener);
@@ -52,29 +51,34 @@ protected void refreshListeners() {
      * Updates the position of the scaler block to match the edge point.
      */
     public void updatePosition() {
-        setLayoutX(decoratorTarget.getEdgePoints().get(index).getValue().getX() - (getWidth() / 2));
-        setLayoutY(decoratorTarget.getEdgePoints().get(index).getValue().getY() - (getHeight() / 2));
+        setLayoutX(
+            decoratorTarget.getEdgePoints().get(index).getValue().getX() - getDecoratorTarget().getPosition().getX() - (
+                getWidth() / 2));
+        setLayoutY(
+            decoratorTarget.getEdgePoints().get(index).getValue().getY() - getDecoratorTarget().getPosition().getY() - (
+                getHeight() / 2));
     }
 
     /**
      * Sets the position of the scaler block and updates the edge point.
      *
      * @param point The new position of the scaler block.
      */
-    public void setPosition(Point2D point) {
+    public void setLayoutPosition(Point2D point) {
         setLayoutX(point.getX());
         setLayoutY(point.getY());
 
         decoratorTarget.setEdgePoint(index, point);
     }
 
     /**
-     * Sets the center position of the scaler block and updates the edge point.
+     * Sets the center position of the scaler in world coordinates block and updates the edge point.
      *
      * @param point The new center of the scaler block.
      */
     public boolean setCenter(Point2D point) {
         if (decoratorTarget.setEdgePoint(index, point)) {
+            point = point.subtract(getDecoratorTarget().getPosition());
             Point2D center = new Point2D(point.getX() - (getWidth() / 2), point.getY() - (getHeight() / 2));
             setLayoutX(center.getX());
             setLayoutY(center.getY());
@@ -88,7 +92,7 @@ public boolean setCenter(Point2D point) {
      *
      * @return The position of the scaler block.
      */
-    public Point2D getPosition() {
+    public Point2D getLayoutPosition() {
         return new Point2D(getLayoutX(), getLayoutY());
     }
 

diff --git a/src/main/java/org/gecko/viewmodel/EditorViewModel.java b/src/main/java/org/gecko/viewmodel/EditorViewModel.java
@@ -45,7 +45,7 @@
  */
 @Data
 public class EditorViewModel {
-    private static final double MAX_ZOOM_SCALE = 3;
+    private static final double MAX_ZOOM_SCALE = 2.5;
     private static final double MIN_ZOOM_SCALE = 0.1;
     private final int id;
     private final ActionManager actionManager;
@@ -262,11 +262,9 @@ public void zoom(double factor, Point2D pivot) {
         if (factor < 0) {
             throw new IllegalArgumentException("Zoom factor must be positive");
         }
+        double oldScale = zoomScaleProperty.get();
         zoomScaleProperty.set((Math.clamp(zoomScaleProperty.get() * factor, MIN_ZOOM_SCALE, MAX_ZOOM_SCALE)));
-        pivot = pivot.multiply(1 / zoomScaleProperty.get());
-        double newX = pivot.getX() * (factor - 1) + factor * pivotProperty.getValue().getX();
-        double newY = pivot.getY() * (factor - 1) + factor * pivotProperty.getValue().getY();
-        setPivot(new Point2D(newX, newY));
+        setPivot(getPivot().add(pivot.subtract(getPivot()).multiply(zoomScaleProperty.get() / oldScale - 1)));
     }
 
     public void zoomCenter(double factor) {