From 6bb601f78e5ce20ad9a0e8705176f22fe79dbb0f Mon Sep 17 00:00:00 2001 From: DecwLK Date: Thu, 7 Mar 2024 13:29:40 +0100 Subject: [PATCH] fix region scaling; fix zoom at mouse cursor --- .../MoveEdgeViewModelElementAction.java | 2 +- ...SystemConnectionViewModelElementAction.java | 2 +- src/main/java/org/gecko/tools/CursorTool.java | 8 ++++---- .../org/gecko/view/views/ViewElementPane.java | 17 +++++++++-------- .../views/viewelement/BlockViewElement.java | 9 +++++---- .../decorator/ElementScalerBlock.java | 18 +++++++++++------- .../org/gecko/viewmodel/EditorViewModel.java | 8 +++----- 7 files changed, 34 insertions(+), 30 deletions(-) diff --git a/src/main/java/org/gecko/actions/MoveEdgeViewModelElementAction.java b/src/main/java/org/gecko/actions/MoveEdgeViewModelElementAction.java index e5e21791..b2cd5e8a 100644 --- 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 index 0ea2f290..e790fd25 100644 --- 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 index bc8b10ac..ec765b80 100644 --- 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 index dbc7c67b..97beaad0 100644 --- 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 index 844be219..284dee9f 100644 --- 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 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 index 6b44761a..a3c9a313 100644 --- 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 newListener = (observable, oldValue, newValue) -> { if (!isDragging) { - setLayoutX(newValue.getX() - (getWidth() / 2)); - setLayoutY(newValue.getY() - (getHeight() / 2)); + updatePosition(); } }; decoratorTarget.getEdgePoints().get(index).addListener(newListener); @@ -52,8 +51,12 @@ 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)); } /** @@ -61,7 +64,7 @@ public void updatePosition() { * * @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()); @@ -69,12 +72,13 @@ public void setPosition(Point2D 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 index d197d222..35bd2b9e 100644 --- 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) {