← Back to branch summary

~tapaal-contributor/tapaal/display-shared-places-transitions-1879126

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/Place.java

  • Committer: Jiri Srba
  • Date: 2020-04-28 19:15:28 UTC
  • mfrom: (998.2.376 testbranch)
  • Revision ID: srba@cs.aau.dk-20200428191528-3xxjqa1r4jcob5ur
merged in lp:~yrke/tapaal/testbranch doing majour refactoring of the GUI

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/graphicElements/Place.java
8
8
import java.awt.geom.Ellipse2D;
9
9
 
10
10
import pipe.gui.CreateGui;
11
 
import pipe.gui.Grid;
12
11
import pipe.gui.Pipe;
13
12
import pipe.gui.Zoomer;
14
13
 
19
18
 
20
19
        private static final long serialVersionUID = -5155964364065651381L;
21
20
 
22
 
 
23
 
        // Value of the capacity restriction; 0 means no capacity restriction 
24
 
        protected Integer capacity = 0;
25
 
 
26
21
        protected static final int DIAMETER = Pipe.PLACE_TRANSITION_HEIGHT;
27
22
 
28
23
        // Token Width and Height
41
36
        protected static Ellipse2D.Double placeEllipse = new Ellipse2D.Double(0, 0,     DIAMETER, DIAMETER);
42
37
        protected static Shape proximityPlace = (new BasicStroke(Pipe.PLACE_TRANSITION_PROXIMITY_RADIUS)).createStrokedShape(placeEllipse);
43
38
 
 
39
 
 
40
        public Place(
 
41
                        int positionXInput,
 
42
                        int positionYInput,
 
43
                        String idInput,
 
44
                        int nameOffsetXInput,
 
45
                        int nameOffsetYInput
 
46
        ){
 
47
                super(positionXInput, positionYInput, idInput,  nameOffsetXInput, nameOffsetYInput);
 
48
                componentWidth = DIAMETER;
 
49
                componentHeight = DIAMETER;
 
50
        }
 
51
 
 
52
        @Deprecated
44
53
        public Place(double positionXInput, double positionYInput, String idInput,
45
 
                        Double nameOffsetXInput, Double nameOffsetYInput) {
46
 
                super(positionXInput, positionYInput, idInput,  nameOffsetXInput, nameOffsetYInput);
47
 
                componentWidth = DIAMETER;
48
 
                componentHeight = DIAMETER;
49
 
                setCentre((int) positionX, (int) positionY);
 
54
                        double nameOffsetXInput, double nameOffsetYInput) {
 
55
                this((int)positionXInput, (int)positionYInput, idInput, (int)nameOffsetXInput, (int)nameOffsetYInput);
50
56
        }
51
57
 
52
 
        
 
58
        @Deprecated
53
59
        public Place(double positionXInput, double positionYInput) {
54
 
                super(positionXInput, positionYInput);
55
 
                componentWidth = DIAMETER;
56
 
                componentHeight = DIAMETER;
57
 
                setCentre((int) positionX, (int) positionY);
 
60
                this((int)positionXInput, (int)positionYInput, null, 0,0);
 
61
        }
 
62
 
 
63
        public Place(int positionXInput, int positionYInput) {
 
64
                this(positionXInput, positionYInput, null, 0,0);
58
65
        }
59
66
 
60
67
        @Override
89
96
         * Returns the diameter of this Place at the current zoom
90
97
         */
91
98
        private int getDiameter() {
92
 
                return (Zoomer.getZoomedValue(DIAMETER, zoom));
 
99
                return (Zoomer.getZoomedValue(DIAMETER, getZoom()));
93
100
        }
94
101
 
95
102
        @Override
96
103
        public boolean contains(int x, int y) {
97
 
                double unZoomedX = Zoomer.getUnzoomedValue(x - COMPONENT_DRAW_OFFSET, zoom);
98
 
                double unZoomedY = Zoomer.getUnzoomedValue(y - COMPONENT_DRAW_OFFSET, zoom);
 
104
                double unZoomedX = Zoomer.getUnzoomedValue(x - COMPONENT_DRAW_OFFSET, getZoom());
 
105
                double unZoomedY = Zoomer.getUnzoomedValue(y - COMPONENT_DRAW_OFFSET, getZoom());
99
106
 
100
 
                Arc someArc = CreateGui.getDrawingSurface().createArc;
101
 
                if (someArc != null) { // Must be drawing a new Arc if non-NULL.
102
 
                        if ((proximityPlace.contains((int) unZoomedX, (int) unZoomedY) || placeEllipse
103
 
                                        .contains((int) unZoomedX, (int) unZoomedY))
104
 
                                        && areNotSameType(someArc.getSource())) {
105
 
                                // assume we are only snapping the target...
106
 
                                if (someArc.getTarget() != this) {
107
 
                                        someArc.setTarget(this);
108
 
                                }
109
 
                                someArc.updateArcPosition();
110
 
                                return true;
111
 
                        } else {
112
 
                                if (someArc.getTarget() == this) {
113
 
                                        someArc.setTarget(null);
114
 
                                        updateConnected();
115
 
                                }
116
 
                                return false;
117
 
                        }
 
107
                Arc createArc = CreateGui.getDrawingSurface().createArc;
 
108
                if (createArc != null) { // Must be drawing a new Arc if non-NULL.
 
109
                        return (proximityPlace.contains((int) unZoomedX, (int) unZoomedY) ||
 
110
                                        placeEllipse.contains((int) unZoomedX, (int) unZoomedY));
118
111
                } else {
119
112
                        return placeEllipse.contains((int) unZoomedX, (int) unZoomedY);
120
113
                }
146
139
        }
147
140
 
148
141
        @Override
149
 
        public void toggleAttributesVisible() {
150
 
                attributesVisible = !attributesVisible;
151
 
                update(true);
152
 
        }
153
 
 
154
 
        @Override
155
 
        public void addedToGui() {
156
 
                super.addedToGui();
157
 
                update(true);
158
 
        }
159
 
 
160
 
        @Override
161
142
        public void update(boolean displayConstantNames) {
162
143
                if (attributesVisible) {
163
 
                        pnName.setText("");
 
144
                        getNameLabel().setText("");
164
145
                } else {
165
 
                        pnName.setText("");
 
146
                        getNameLabel().setText("");
166
147
                }
167
 
                pnName.zoomUpdate(zoom);
168
148
                super.update(displayConstantNames);
169
149
                repaint();
170
150
        }