Merge pull request #124 from DecwLK/zoom_pan_rewrite

Zoom pan rewrite
DecwLK · Mar 7, 2024 · 76defa0 · 76defa0
2 parents 541521c + 6bb601f
commit 76defa0
Show file tree

Hide file tree

Showing 32 changed files with 470 additions and 526 deletions.
diff --git a/src/main/java/org/gecko/actions/ActionFactory.java b/src/main/java/org/gecko/actions/ActionFactory.java
@@ -106,11 +106,11 @@ public CreateSystemConnectionViewModelElementAction createCreateSystemConnection
     }
 
     public CreateSystemViewModelElementAction createCreateSystemViewModelElementAction(Point2D position) {
-        return new CreateSystemViewModelElementAction(geckoViewModel, geckoViewModel.getCurrentEditor(), position);
+        return new CreateSystemViewModelElementAction(geckoViewModel, position);
     }
 
     public CreateVariableAction createCreateVariableAction(Point2D position) {
-        return new CreateVariableAction(geckoViewModel, geckoViewModel.getCurrentEditor(), position);
+        return new CreateVariableAction(geckoViewModel, position);
     }
 
     public DeleteContractViewModelAction createDeleteContractViewModelAction(

diff --git a/src/main/java/org/gecko/actions/CreateStateViewModelElementAction.java b/src/main/java/org/gecko/actions/CreateStateViewModelElementAction.java
@@ -31,7 +31,7 @@ public class CreateStateViewModelElementAction extends Action {
     boolean run() throws GeckoException {
         SystemViewModel currentParentSystem = geckoViewModel.getCurrentEditor().getCurrentSystem();
         createdStateViewModel = geckoViewModel.getViewModelFactory().createStateViewModelIn(currentParentSystem);
-        createdStateViewModel.setCenter(editorViewModel.transformViewPortToWorldCoordinates(position));
+        createdStateViewModel.setCenter(position);
         editorViewModel.updateRegions();
         ActionManager actionManager = geckoViewModel.getActionManager();
         actionManager.run(actionManager.getActionFactory().createSelectAction(createdStateViewModel, true));

diff --git a/src/main/java/org/gecko/actions/CreateSystemViewModelElementAction.java b/src/main/java/org/gecko/actions/CreateSystemViewModelElementAction.java
@@ -15,23 +15,20 @@
 public class CreateSystemViewModelElementAction extends Action {
 
     private final GeckoViewModel geckoViewModel;
-    private final EditorViewModel editorViewModel;
     private final Point2D position;
     private SystemViewModel createdSystemViewModel;
 
     CreateSystemViewModelElementAction(
-        GeckoViewModel geckoViewModel, EditorViewModel editorViewModel, Point2D position) {
+        GeckoViewModel geckoViewModel, Point2D position) {
         this.geckoViewModel = geckoViewModel;
-        this.editorViewModel = editorViewModel;
         this.position = position;
     }
 
     @Override
     boolean run() throws GeckoException {
         SystemViewModel currentParentSystem = geckoViewModel.getCurrentEditor().getCurrentSystem();
         createdSystemViewModel = geckoViewModel.getViewModelFactory().createSystemViewModelIn(currentParentSystem);
-        Point2D pos = editorViewModel.transformViewPortToWorldCoordinates(position);
-        createdSystemViewModel.setCenter(pos);
+        createdSystemViewModel.setCenter(position);
         ActionManager actionManager = geckoViewModel.getActionManager();
         actionManager.run(actionManager.getActionFactory().createSelectAction(createdSystemViewModel, true));
         return true;

diff --git a/src/main/java/org/gecko/actions/CreateVariableAction.java b/src/main/java/org/gecko/actions/CreateVariableAction.java
@@ -16,21 +16,19 @@
 public class CreateVariableAction extends Action {
 
     private final GeckoViewModel geckoViewModel;
-    private final EditorViewModel editorViewModel;
     private final Point2D position;
     private PortViewModel createdPortViewModel;
 
-    CreateVariableAction(GeckoViewModel geckoViewModel, EditorViewModel editorViewModel, Point2D position) {
+    CreateVariableAction(GeckoViewModel geckoViewModel, Point2D position) {
         this.geckoViewModel = geckoViewModel;
-        this.editorViewModel = editorViewModel;
         this.position = position;
     }
 
     @Override
     boolean run() throws GeckoException {
         createdPortViewModel = geckoViewModel.getViewModelFactory()
             .createPortViewModelIn(geckoViewModel.getCurrentEditor().getCurrentSystem());
-        createdPortViewModel.setCenter(editorViewModel.transformViewPortToWorldCoordinates(position));
+        createdPortViewModel.setCenter(position);
         ActionManager actionManager = geckoViewModel.getActionManager();
         actionManager.run(actionManager.getActionFactory().createSelectAction(createdPortViewModel, true));
         return true;

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/actions/ZoomAction.java b/src/main/java/org/gecko/actions/ZoomAction.java
@@ -22,7 +22,7 @@ public class ZoomAction extends Action {
 
     @Override
     boolean run() throws GeckoException {
-        editorViewModel.zoom(pivot, factor);
+        editorViewModel.zoom(factor, pivot);
         return true;
     }
 

diff --git a/src/main/java/org/gecko/io/AutomatonFileVisitor.java b/src/main/java/org/gecko/io/AutomatonFileVisitor.java
@@ -178,6 +178,10 @@ public String visitAutomata(SystemDefParser.AutomataContext ctx) {
         if (!ctx.use_contracts().isEmpty()) {
             warnings.add("Automaton %s has use_contracts, which are be ignored".formatted(ctx.ident().getText()));
         }
+        if (ctx.transition().isEmpty()) {
+            warnings.add("Automaton %s has no transitions".formatted(ctx.ident().getText()));
+            return null;
+        }
         for (SystemDefParser.TransitionContext transition : ctx.transition()) {
             String result = transition.accept(this);
             if (result != null) {
@@ -197,6 +201,13 @@ public String visitAutomata(SystemDefParser.AutomataContext ctx) {
             } catch (ModelException e) {
                 return e.getMessage();
             }
+        } else {
+            try {
+                //this should always work because if we have a transition, we have a state
+                currentSystem.getAutomaton().setStartState(currentSystem.getAutomaton().getStates().iterator().next());
+            } catch (ModelException e) {
+                throw new RuntimeException(e);
+            }
         }
         return null;
     }
@@ -355,7 +366,9 @@ private System buildSystem(SystemDefParser.SystemContext ctx) throws GeckoExcept
     }
 
     private Contract buildContract(State state, SystemDefParser.PrepostContext contract) throws GeckoException {
-        return buildContract(state, contract.pre.getText(), contract.post.getText());
+        Contract c = buildContract(state, contract.pre.getText(), contract.post.getText());
+        c.setName(contract.name.getText());
+        return c;
     }
 
     private Contract buildContract(State state, String pre, String post) throws GeckoException {

diff --git a/src/main/java/org/gecko/tools/AreaTool.java b/src/main/java/org/gecko/tools/AreaTool.java
@@ -4,13 +4,13 @@
 import javafx.geometry.Bounds;
 import javafx.geometry.Point2D;
 import javafx.scene.Cursor;
-import javafx.scene.Group;
 import javafx.scene.control.ScrollPane;
 import javafx.scene.input.MouseButton;
 import javafx.scene.input.MouseEvent;
-import javafx.scene.layout.VBox;
+import javafx.scene.layout.Pane;
 import javafx.scene.shape.Rectangle;
 import org.gecko.actions.ActionManager;
+import org.gecko.view.views.ViewElementPane;
 
 /**
  * A concrete representation of an area-{@link Tool}, utilized for marking a rectangle-formed area in the view. Holds
@@ -19,71 +19,69 @@
 public abstract class AreaTool extends Tool {
 
     private Point2D startPosition;
+    private Point2D startScreenPosition;
     private Rectangle area;
+    private ScrollPane view;
 
     public AreaTool(ActionManager actionManager, ToolType toolType) {
         super(actionManager, toolType);
     }
 
     @Override
-    public void visitView(VBox vbox, ScrollPane view, Group worldGroup, Group containerGroup) {
-        super.visitView(vbox, view, worldGroup, containerGroup);
+    public void visitView(ViewElementPane pane) {
+        super.visitView(pane);
+        view = pane.draw();
+        Pane world = pane.getWorld();
         view.setPannable(false);
         view.setCursor(Cursor.CROSSHAIR);
-        worldGroup.setMouseTransparent(true);
         startPosition = null;
 
-        vbox.setOnMousePressed(event -> {
+        world.setOnMousePressed(event -> {
             if (event.getButton() != MouseButton.PRIMARY) {
                 return;
             }
-
-            startPosition = containerGroup.sceneToLocal(event.getSceneX(), event.getSceneY());
+            startPosition = pane.screenToLocalCoordinates(event.getScreenX(), event.getScreenY());
+            startScreenPosition = new Point2D(event.getScreenX(), event.getScreenY());
             area = createNewArea();
             area.setX(startPosition.getX());
             area.setY(startPosition.getY());
-            containerGroup.getChildren().add(area);
+            world.getChildren().add(area);
         });
 
-        vbox.setOnMouseDragged(event -> {
+        world.setOnMouseDragged(event -> {
             if (startPosition == null) {
                 return;
             }
-            Bounds areaBounds = calculateAreaBounds(startPosition,
-                containerGroup.sceneToLocal(new Point2D(event.getSceneX(), event.getSceneY())));
+            Point2D dragPosition = pane.screenToLocalCoordinates(event.getScreenX(), event.getScreenY());
+            Bounds areaBounds = calculateAreaBounds(startPosition, dragPosition);
             area.setX(areaBounds.getMinX());
             area.setY(areaBounds.getMinY());
             area.setWidth(areaBounds.getWidth());
             area.setHeight(areaBounds.getHeight());
         });
 
-        vbox.setOnMouseReleased(event -> {
+        world.setOnMouseReleased(event -> {
             if (startPosition == null) {
                 return;
             }
-            containerGroup.getChildren().remove(area);
-            Bounds areaBounds = calculateAreaBounds(getStartPosition(),
-                containerGroup.sceneToLocal(new Point2D(event.getSceneX(), event.getSceneY())));
-            Bounds worldAreaBounds = worldGroup.sceneToLocal(containerGroup.localToScene(areaBounds));
-            onAreaCreated(event, worldAreaBounds);
+            world.getChildren().remove(area);
+            Point2D endPos = pane.screenToWorldCoordinates(event.getScreenX(), event.getScreenY());
+            onAreaCreated(event, calculateAreaBounds(pane.screenToWorldCoordinates(startScreenPosition), endPos));
             startPosition = null;
+            startScreenPosition = null;
         });
     }
 
-    abstract Rectangle createNewArea();
-
-    protected Bounds calculateAreaBounds(Point2D startPosition, Point2D eventPosition) {
-        Point2D topLeft = new Point2D(Math.min(startPosition.getX(), eventPosition.getX()),
-            Math.min(startPosition.getY(), eventPosition.getY()));
-        Point2D bottomRight = new Point2D(Math.max(startPosition.getX(), eventPosition.getX()),
-            Math.max(startPosition.getY(), eventPosition.getY()));
+    protected Bounds calculateAreaBounds(Point2D startPosition, Point2D endPosition) {
+        Point2D topLeft = new Point2D(Math.min(startPosition.getX(), endPosition.getX()),
+            Math.min(startPosition.getY(), endPosition.getY()));
+        Point2D bottomRight = new Point2D(Math.max(startPosition.getX(), endPosition.getX()),
+            Math.max(startPosition.getY(), endPosition.getY()));
         return new BoundingBox(topLeft.getX(), topLeft.getY(), bottomRight.getX() - topLeft.getX(),
             bottomRight.getY() - topLeft.getY());
     }
 
-    abstract void onAreaCreated(MouseEvent event, Bounds worldAreaBounds);
+    abstract Rectangle createNewArea();
 
-    protected Point2D getStartPosition() {
-        return startPosition;
-    }
+    abstract void onAreaCreated(MouseEvent event, Bounds worldBounds);
 }