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

Proposed by Kenneth Yrke Jørgensen on 2019-05-09
Status: Merged
Approved by: Jiri Srba on 2019-05-21
Approved revision: 1002
Merged at revision: 1010
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
Jiri Srba 2019-05-09 Approve on 2019-05-21
Review via email: mp+367176@code.launchpad.net

This proposal supersedes a proposal from 2019-05-09.

Commit message

Fixed bug 1827039, constant hightlight not working

Fixed bug where hightlight of constants was not working, after refactoring. The color hightlight was overwritten in drawComponent. Now select() and hightlight() sets the color of lable correctly

Also arcs now uses the pnName label over the lable.

To post a comment you must log in.
Jiri Srba (srba) wrote :

Tested and highlighting constants works again.

review: Approve

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:08:10 +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:08:10 +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:08:10 +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:08:10 +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:08:10 +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:08:10 +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:08:10 +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:08:10 +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:08:10 +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