← Back to branch summary

~tapaal-contributor/tapaal/align-to-grid

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/gui/undo/MovePlaceTransitionObject.java

  • Committer: Jiri Srba
  • Date: 2019-08-16 16:00:59 UTC
  • mfrom: (1009.1.50 SmartDrawDec)
  • Revision ID: srba@cs.aau.dk-20190816160059-m3gs4m69szmspr1x
merged in lp:~tapaal-contributor/tapaal/SmartDrawDevelopment allowing for automatic net layout

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/gui/undo/MovePlaceTransitionObject.java
 
1
package dk.aau.cs.gui.undo;
 
2
 
 
3
import java.awt.Point;
 
4
import java.util.Iterator;
 
5
 
 
6
import pipe.gui.CreateGui;
 
7
import pipe.gui.graphicElements.Arc;
 
8
import pipe.gui.graphicElements.Place;
 
9
import pipe.gui.graphicElements.PlaceTransitionObject;
 
10
import pipe.gui.graphicElements.Transition;
 
11
 
 
12
public class MovePlaceTransitionObject extends Command {
 
13
        
 
14
        private double newY;
 
15
        private double newX;
 
16
        private PlaceTransitionObject objectToBeMoved;
 
17
        private double oldY;
 
18
        private double oldX;
 
19
        private boolean doUpdate = false;
 
20
        
 
21
        
 
22
        public MovePlaceTransitionObject(PlaceTransitionObject object, Point point) {
 
23
                objectToBeMoved = object;
 
24
                this.newX = point.getX();
 
25
                this.newY = point.getY();
 
26
                
 
27
        }
 
28
 
 
29
        @Override
 
30
        public void undo() {
 
31
                objectToBeMoved.setPositionX(oldX);
 
32
                objectToBeMoved.setPositionY(oldY);
 
33
                
 
34
                
 
35
                objectToBeMoved.updateOnMoveOrZoom();
 
36
                objectToBeMoved.repaint();
 
37
                CreateGui.getDrawingSurface().updatePreferredSize();
 
38
        }
 
39
 
 
40
        @Override
 
41
        public void redo() {
 
42
                oldY = objectToBeMoved.getPositionY();
 
43
                oldX = objectToBeMoved.getPositionX();
 
44
                
 
45
                objectToBeMoved.setPositionX(newX);
 
46
                objectToBeMoved.setPositionY(newY);
 
47
                
 
48
                if(doUpdate) {
 
49
                        objectToBeMoved.updateOnMoveOrZoom();
 
50
                        objectToBeMoved.repaint();
 
51
                        CreateGui.getDrawingSurface().updatePreferredSize();
 
52
                }
 
53
                doUpdate = true;
 
54
                
 
55
        }
 
56
 
 
57
}