TAPAAL

Merge lp:~yrke/tapaal/tapaal-fix1827039-constantHightlight into lp:tapaal

  1. tapaal-fix1827039-constantHightlight
  2. Merge into trunk
Proposed by Kenneth Yrke Jørgensen
Status: Superseded
Proposed branch: lp:~yrke/tapaal/tapaal-fix1827039-constantHightlight
Merge into: lp:tapaal
Diff against target: 358 lines (+64/-44)
9 files modified
src/pipe/gui/graphicElements/Arc.java (+17/-16)
src/pipe/gui/graphicElements/PetriNetObject.java (+12/-1)
src/pipe/gui/graphicElements/Place.java (+2/-2)
src/pipe/gui/graphicElements/PlaceTransitionObject.java (+4/-0)
src/pipe/gui/graphicElements/Transition.java (+2/-2)
src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java (+4/-4)
src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java (+11/-9)
src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java (+2/-2)
src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java (+10/-8)
To merge this branch: bzr merge lp:~yrke/tapaal/tapaal-fix1827039-constantHightlight
Reviewer Review Type Date Requested Status
TAPAAL Reviewers Pending
Review via email: mp+367175@code.launchpad.net

This proposal has been superseded by a proposal from 2019-05-09.

To post a comment you must log in.

Unmerged revisions

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/pipe/gui/graphicElements/Arc.java'
2--- src/pipe/gui/graphicElements/Arc.java 2019-03-13 07:27:29 +0000
3+++ src/pipe/gui/graphicElements/Arc.java 2019-05-09 09:07:50 +0000
4@@ -28,7 +28,7 @@
5 0, -10, -7, -10 }, 4);
6 protected boolean fillHead = true; //If true, fill the shape when drawing, if false, fill with bg color.
7
8- protected NameLabel label;
9+ //protected NameLabel label;
10
11 private static Point2D.Double point;
12
13@@ -62,7 +62,7 @@
14 double endPositionXInput, double endPositionYInput,
15 PlaceTransitionObject sourceInput,
16 PlaceTransitionObject targetInput, int weightInput, String idInput) {
17- label = new NameLabel(zoom);
18+ pnName = new NameLabel(zoom);
19 myPath.addPoint((float) startPositionXInput,
20 (float) startPositionYInput, ArcPathPoint.STRAIGHT);
21 myPath.addPoint((float) endPositionXInput, (float) endPositionYInput,
22@@ -83,7 +83,7 @@
23 */
24 public Arc(PlaceTransitionObject newSource) {
25 isPrototype = true;
26- label = new NameLabel(zoom);
27+ pnName = new NameLabel(zoom);
28 source = newSource;
29 myPath.addPoint();
30 myPath.addPoint();
31@@ -96,7 +96,7 @@
32 public Arc() {
33 super();
34
35- label = new NameLabel(zoom);
36+ pnName = new NameLabel(zoom);
37 //XXX see comment in function
38 setLableHandler();
39 }
40@@ -138,7 +138,8 @@
41 }
42
43 public void setLabelPosition() {
44- label.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
45+
46+ pnName.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
47 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));
48 }
49 @Override
50@@ -170,7 +171,7 @@
51
52 @Override
53 public NameLabel getNameLabel() {
54- return label;
55+ return pnName;
56 }
57
58 /**
59@@ -279,10 +280,10 @@
60 //Draw Path
61 if (selected) {
62 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);
63- this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
64+ //this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
65 } else {
66 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);
67- this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
68+ //this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
69 }
70
71 g2.setStroke(new BasicStroke(0.01f * zoom));
72@@ -302,10 +303,10 @@
73
74 if (selected) {
75 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);
76- this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
77+ //this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
78 } else {
79 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);
80- this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
81+ //this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
82 }
83
84 g2.setStroke(new BasicStroke(0.8f));
85@@ -350,8 +351,8 @@
86 myPath.addPointsToGui((DrawingSurfaceImpl) getParent());
87
88 updateArcPosition();
89- if (getParent() != null && label.getParent() == null) {
90- getParent().add(label);
91+ if (getParent() != null && pnName.getParent() == null) {
92+ getParent().add(pnName);
93 }
94 }
95
96@@ -359,7 +360,7 @@
97 public void delete() {
98 if (!deleted) {
99 if (getParent() != null) {
100- getParent().remove(label);
101+ getParent().remove(pnName);
102 }
103 if(source != null) source.removeFromArc(this);
104 if(target != null) target.removeToArc(this);
105@@ -388,7 +389,7 @@
106
107 public void removeFromView() {
108 if (getParent() != null) {
109- getParent().remove(label);
110+ getParent().remove(pnName);
111 }
112 myPath.forceHidePoints();
113 removeFromContainer();
114@@ -429,8 +430,8 @@
115 zoom = percent;
116 this.updateArcPosition();
117 this.updateOnMoveOrZoom();
118- label.zoomUpdate(percent);
119- label.updateSize();
120+ pnName.zoomUpdate(percent);
121+ pnName.updateSize();
122 }
123
124 public void setZoom(int percent) {
125
126=== modified file 'src/pipe/gui/graphicElements/PetriNetObject.java'
127--- src/pipe/gui/graphicElements/PetriNetObject.java 2019-03-13 07:27:29 +0000
128+++ src/pipe/gui/graphicElements/PetriNetObject.java 2019-05-09 09:07:50 +0000
129@@ -219,17 +219,28 @@
130 }
131
132 public void select(boolean shouldRepaint) {
133- if (selectable && !selected) {
134+ if (selectable && !selected) {
135 selected = true;
136+
137+ if (pnName != null) {
138+ pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
139+ }
140+
141 if (shouldRepaint) {
142 repaint();
143 }
144 }
145+
146 }
147
148 public void deselect() {
149 if (selected) {
150 selected = false;
151+
152+ if (pnName != null) {
153+ pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
154+ }
155+
156 repaint();
157 }
158 }
159
160=== modified file 'src/pipe/gui/graphicElements/Place.java'
161--- src/pipe/gui/graphicElements/Place.java 2019-03-13 08:30:09 +0000
162+++ src/pipe/gui/graphicElements/Place.java 2019-05-09 09:07:50 +0000
163@@ -68,10 +68,10 @@
164
165 if (selected) {
166 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
167- pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
168+ //pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
169 } else {
170 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
171- pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
172+ //pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
173 }
174 g2.fill(placeEllipse);
175
176
177=== modified file 'src/pipe/gui/graphicElements/PlaceTransitionObject.java'
178--- src/pipe/gui/graphicElements/PlaceTransitionObject.java 2018-10-21 18:14:13 +0000
179+++ src/pipe/gui/graphicElements/PlaceTransitionObject.java 2019-05-09 09:07:50 +0000
180@@ -320,6 +320,10 @@
181 if (selectable && !selected) {
182 selected = true;
183
184+ if (pnName != null) {
185+ pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
186+ }
187+
188 // Select arcs that are connected from this object to another selected object.
189 for (Arc arc : getPostset()) {
190 if(arc.getTarget().isSelected()){
191
192=== modified file 'src/pipe/gui/graphicElements/Transition.java'
193--- src/pipe/gui/graphicElements/Transition.java 2019-03-13 07:27:29 +0000
194+++ src/pipe/gui/graphicElements/Transition.java 2019-05-09 09:07:50 +0000
195@@ -97,10 +97,10 @@
196
197 if (selected) {
198 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
199- pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
200+ //pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
201 } else {
202 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
203- pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
204+ //pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
205 }
206
207 if (highlighted) {
208
209=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java'
210--- src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java 2019-03-13 07:27:29 +0000
211+++ src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java 2019-05-09 09:07:50 +0000
212@@ -80,9 +80,9 @@
213
214 @Override
215 public void updateLabel(boolean displayConstantNames) {
216- label.setText("");
217+ pnName.setText("");
218 if(getWeight().value() > 1 || displayConstantNames){
219- label.setText(getWeight().toString(displayConstantNames));
220+ pnName.setText(getWeight().toString(displayConstantNames));
221 }
222
223 boolean focusedConstant = false;
224@@ -92,9 +92,9 @@
225 }
226 }
227 if(focusedConstant){
228- label.setForeground(Pipe.SELECTION_TEXT_COLOUR);
229+ pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
230 }else{
231- label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
232+ pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
233 }
234
235 this.setLabelPosition();
236
237=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java'
238--- src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2018-10-18 15:08:44 +0000
239+++ src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2019-05-09 09:07:50 +0000
240@@ -120,21 +120,21 @@
241 }
242 if (!CreateGui.getModel().netType().equals(NetType.UNTIMED)) {
243 if (inputArc == null)
244- label.setText("");
245+ pnName.setText("");
246 else {
247 if (!CreateGui.getApp().showZeroToInfinityIntervals()) {
248 if (inputArc.interval().toString(showConstantNames).equals("[0,inf)")){
249- label.setText("");
250+ pnName.setText("");
251 }
252 else {
253- label.setText(inputArc.interval().toString(showConstantNames));
254+ pnName.setText(inputArc.interval().toString(showConstantNames));
255 }
256 }
257 else {
258- label.setText(inputArc.interval().toString(showConstantNames));
259+ pnName.setText(inputArc.interval().toString(showConstantNames));
260 }
261-
262- label.setText(getWeight().toString(showConstantNames)+" "+label.getText());
263+
264+ pnName.setText(getWeight().toString(showConstantNames)+" "+pnName.getText());
265
266 // Handle constant highlighting
267 boolean focusedConstant = false;
268@@ -154,9 +154,9 @@
269 }
270 }
271 if(focusedConstant){
272- label.setForeground(Pipe.SELECTION_TEXT_COLOUR);
273+ pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
274 }else{
275- label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
276+ pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
277 }
278
279 }
280@@ -169,8 +169,10 @@
281 /*label.setPosition((int) (myPath.midPoint.x + nameOffsetX)
282 + label.getWidth() / 2 - 4, (int) (myPath.midPoint.y + nameOffsetY)
283 - ((zoom / 55) * (zoom / 55)));*/
284- label.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
285+
286+ pnName.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
287 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));
288+
289 }
290
291 public dk.aau.cs.model.tapn.TimedInputArc underlyingTimedInputArc() {
292
293=== modified file 'src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java'
294--- src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2019-03-16 13:57:33 +0000
295+++ src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2019-05-09 09:07:50 +0000
296@@ -133,8 +133,8 @@
297 }
298
299 public void updateLabel(boolean displayConstantNames) {
300- label.setText("");
301- label.setText(getWeight().toString(displayConstantNames)+" " + label.getText());
302+ pnName.setText("");
303+ pnName.setText(getWeight().toString(displayConstantNames)+" " + pnName.getText());
304 setLabelPosition();
305 }
306
307
308=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java'
309--- src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java 2019-01-27 12:49:43 +0000
310+++ src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java 2019-05-09 09:07:50 +0000
311@@ -97,17 +97,19 @@
312 public void updateLabel(boolean displayConstantNames) {
313 if (isInPreSet && underlyingTransportArc != null) {
314 if (CreateGui.getApp().showZeroToInfinityIntervals()){
315- label.setText(underlyingTransportArc.interval().toString(
316+ pnName.setText(underlyingTransportArc.interval().toString(
317 displayConstantNames)
318 + " : " + getGroup());
319 }
320 else {
321 if (underlyingTransportArc.interval().toString(
322 displayConstantNames).equals("[0,inf)")) {
323- label.setText(" : " + String.valueOf(getGroup()));
324+
325+ pnName.setText(" : " + String.valueOf(getGroup()));
326+
327 }
328 else {
329- label.setText(underlyingTransportArc.interval().toString(
330+ pnName.setText(underlyingTransportArc.interval().toString(
331 displayConstantNames)
332 + " : " + getGroup());
333 }
334@@ -131,19 +133,19 @@
335 }
336 }
337 if(focusedConstant){
338- label.setForeground(Pipe.SELECTION_TEXT_COLOUR);
339+ pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
340 }else{
341- label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
342+ pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
343 }
344
345 } else if (!isInPreSet) {
346- label.setText(" : " + String.valueOf(getGroup()));
347+ pnName.setText(" : " + String.valueOf(getGroup()));
348 } else {
349- label.setText("");
350+ pnName.setText("");
351 }
352
353 if(underlyingTransportArc != null){
354- label.setText(getWeight().toString(displayConstantNames)+" "+label.getText());
355+ pnName.setText(getWeight().toString(displayConstantNames)+" "+pnName.getText());
356 }
357
358 this.setLabelPosition();

Subscribers

People subscribed via source and target branches