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
=== modified file 'src/pipe/gui/graphicElements/Arc.java'
--- src/pipe/gui/graphicElements/Arc.java 2019-03-13 07:27:29 +0000
+++ src/pipe/gui/graphicElements/Arc.java 2019-05-09 09:07:50 +0000
@@ -28,7 +28,7 @@
28 0, -10, -7, -10 }, 4);28 0, -10, -7, -10 }, 4);
29 protected boolean fillHead = true; //If true, fill the shape when drawing, if false, fill with bg color.29 protected boolean fillHead = true; //If true, fill the shape when drawing, if false, fill with bg color.
3030
31 protected NameLabel label;31 //protected NameLabel label;
3232
33 private static Point2D.Double point;33 private static Point2D.Double point;
3434
@@ -62,7 +62,7 @@
62 double endPositionXInput, double endPositionYInput,62 double endPositionXInput, double endPositionYInput,
63 PlaceTransitionObject sourceInput,63 PlaceTransitionObject sourceInput,
64 PlaceTransitionObject targetInput, int weightInput, String idInput) {64 PlaceTransitionObject targetInput, int weightInput, String idInput) {
65 label = new NameLabel(zoom);65 pnName = new NameLabel(zoom);
66 myPath.addPoint((float) startPositionXInput,66 myPath.addPoint((float) startPositionXInput,
67 (float) startPositionYInput, ArcPathPoint.STRAIGHT);67 (float) startPositionYInput, ArcPathPoint.STRAIGHT);
68 myPath.addPoint((float) endPositionXInput, (float) endPositionYInput,68 myPath.addPoint((float) endPositionXInput, (float) endPositionYInput,
@@ -83,7 +83,7 @@
83 */83 */
84 public Arc(PlaceTransitionObject newSource) {84 public Arc(PlaceTransitionObject newSource) {
85 isPrototype = true;85 isPrototype = true;
86 label = new NameLabel(zoom);86 pnName = new NameLabel(zoom);
87 source = newSource;87 source = newSource;
88 myPath.addPoint();88 myPath.addPoint();
89 myPath.addPoint();89 myPath.addPoint();
@@ -96,7 +96,7 @@
96 public Arc() {96 public Arc() {
97 super();97 super();
9898
99 label = new NameLabel(zoom);99 pnName = new NameLabel(zoom);
100 //XXX see comment in function100 //XXX see comment in function
101 setLableHandler();101 setLableHandler();
102 }102 }
@@ -138,7 +138,8 @@
138 }138 }
139139
140 public void setLabelPosition() {140 public void setLabelPosition() {
141 label.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))), 141
142 pnName.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
142 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));143 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));
143 }144 }
144 @Override145 @Override
@@ -170,7 +171,7 @@
170 171
171 @Override 172 @Override
172 public NameLabel getNameLabel() {173 public NameLabel getNameLabel() {
173 return label;174 return pnName;
174 }175 }
175176
176 /**177 /**
@@ -279,10 +280,10 @@
279 //Draw Path280 //Draw Path
280 if (selected) {281 if (selected) {
281 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);282 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);
282 this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);283 //this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
283 } else {284 } else {
284 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);285 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);
285 this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);286 //this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
286 }287 }
287288
288 g2.setStroke(new BasicStroke(0.01f * zoom));289 g2.setStroke(new BasicStroke(0.01f * zoom));
@@ -302,10 +303,10 @@
302303
303 if (selected) {304 if (selected) {
304 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);305 g2.setPaint(Pipe.SELECTION_LINE_COLOUR);
305 this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);306 //this.label.setForeground(Pipe.SELECTION_LINE_COLOUR);
306 } else {307 } else {
307 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);308 g2.setPaint(Pipe.ELEMENT_LINE_COLOUR);
308 this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);309 //this.label.setForeground(Pipe.ELEMENT_LINE_COLOUR);
309 }310 }
310311
311 g2.setStroke(new BasicStroke(0.8f));312 g2.setStroke(new BasicStroke(0.8f));
@@ -350,8 +351,8 @@
350 myPath.addPointsToGui((DrawingSurfaceImpl) getParent());351 myPath.addPointsToGui((DrawingSurfaceImpl) getParent());
351352
352 updateArcPosition();353 updateArcPosition();
353 if (getParent() != null && label.getParent() == null) {354 if (getParent() != null && pnName.getParent() == null) {
354 getParent().add(label);355 getParent().add(pnName);
355 }356 }
356 }357 }
357358
@@ -359,7 +360,7 @@
359 public void delete() {360 public void delete() {
360 if (!deleted) {361 if (!deleted) {
361 if (getParent() != null) {362 if (getParent() != null) {
362 getParent().remove(label);363 getParent().remove(pnName);
363 }364 }
364 if(source != null) source.removeFromArc(this);365 if(source != null) source.removeFromArc(this);
365 if(target != null) target.removeToArc(this);366 if(target != null) target.removeToArc(this);
@@ -388,7 +389,7 @@
388389
389 public void removeFromView() {390 public void removeFromView() {
390 if (getParent() != null) {391 if (getParent() != null) {
391 getParent().remove(label);392 getParent().remove(pnName);
392 }393 }
393 myPath.forceHidePoints();394 myPath.forceHidePoints();
394 removeFromContainer();395 removeFromContainer();
@@ -429,8 +430,8 @@
429 zoom = percent;430 zoom = percent;
430 this.updateArcPosition();431 this.updateArcPosition();
431 this.updateOnMoveOrZoom();432 this.updateOnMoveOrZoom();
432 label.zoomUpdate(percent);433 pnName.zoomUpdate(percent);
433 label.updateSize();434 pnName.updateSize();
434 }435 }
435436
436 public void setZoom(int percent) {437 public void setZoom(int percent) {
437438
=== modified file 'src/pipe/gui/graphicElements/PetriNetObject.java'
--- src/pipe/gui/graphicElements/PetriNetObject.java 2019-03-13 07:27:29 +0000
+++ src/pipe/gui/graphicElements/PetriNetObject.java 2019-05-09 09:07:50 +0000
@@ -219,17 +219,28 @@
219 }219 }
220220
221 public void select(boolean shouldRepaint) {221 public void select(boolean shouldRepaint) {
222 if (selectable && !selected) {222 if (selectable && !selected) {
223 selected = true;223 selected = true;
224
225 if (pnName != null) {
226 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
227 }
228
224 if (shouldRepaint) {229 if (shouldRepaint) {
225 repaint();230 repaint();
226 }231 }
227 }232 }
233
228 }234 }
229235
230 public void deselect() {236 public void deselect() {
231 if (selected) {237 if (selected) {
232 selected = false;238 selected = false;
239
240 if (pnName != null) {
241 pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
242 }
243
233 repaint();244 repaint();
234 }245 }
235 }246 }
236247
=== modified file 'src/pipe/gui/graphicElements/Place.java'
--- src/pipe/gui/graphicElements/Place.java 2019-03-13 08:30:09 +0000
+++ src/pipe/gui/graphicElements/Place.java 2019-05-09 09:07:50 +0000
@@ -68,10 +68,10 @@
6868
69 if (selected) {69 if (selected) {
70 g2.setColor(Pipe.SELECTION_FILL_COLOUR);70 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
71 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);71 //pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
72 } else {72 } else {
73 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);73 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
74 pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);74 //pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
75 }75 }
76 g2.fill(placeEllipse);76 g2.fill(placeEllipse);
7777
7878
=== modified file 'src/pipe/gui/graphicElements/PlaceTransitionObject.java'
--- src/pipe/gui/graphicElements/PlaceTransitionObject.java 2018-10-21 18:14:13 +0000
+++ src/pipe/gui/graphicElements/PlaceTransitionObject.java 2019-05-09 09:07:50 +0000
@@ -320,6 +320,10 @@
320 if (selectable && !selected) {320 if (selectable && !selected) {
321 selected = true;321 selected = true;
322322
323 if (pnName != null) {
324 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
325 }
326
323 // Select arcs that are connected from this object to another selected object.327 // Select arcs that are connected from this object to another selected object.
324 for (Arc arc : getPostset()) {328 for (Arc arc : getPostset()) {
325 if(arc.getTarget().isSelected()){329 if(arc.getTarget().isSelected()){
326330
=== modified file 'src/pipe/gui/graphicElements/Transition.java'
--- src/pipe/gui/graphicElements/Transition.java 2019-03-13 07:27:29 +0000
+++ src/pipe/gui/graphicElements/Transition.java 2019-05-09 09:07:50 +0000
@@ -97,10 +97,10 @@
9797
98 if (selected) {98 if (selected) {
99 g2.setColor(Pipe.SELECTION_FILL_COLOUR);99 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
100 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);100 //pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
101 } else {101 } else {
102 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);102 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
103 pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);103 //pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
104 }104 }
105105
106 if (highlighted) {106 if (highlighted) {
107107
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java 2019-03-13 07:27:29 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedInhibitorArcComponent.java 2019-05-09 09:07:50 +0000
@@ -80,9 +80,9 @@
8080
81 @Override81 @Override
82 public void updateLabel(boolean displayConstantNames) {82 public void updateLabel(boolean displayConstantNames) {
83 label.setText("");83 pnName.setText("");
84 if(getWeight().value() > 1 || displayConstantNames){84 if(getWeight().value() > 1 || displayConstantNames){
85 label.setText(getWeight().toString(displayConstantNames));85 pnName.setText(getWeight().toString(displayConstantNames));
86 }86 }
87 87
88 boolean focusedConstant = false;88 boolean focusedConstant = false;
@@ -92,9 +92,9 @@
92 }92 }
93 }93 }
94 if(focusedConstant){94 if(focusedConstant){
95 label.setForeground(Pipe.SELECTION_TEXT_COLOUR);95 pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
96 }else{96 }else{
97 label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);97 pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
98 }98 }
99 99
100 this.setLabelPosition();100 this.setLabelPosition();
101101
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2018-10-18 15:08:44 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java 2019-05-09 09:07:50 +0000
@@ -120,21 +120,21 @@
120 }120 }
121 if (!CreateGui.getModel().netType().equals(NetType.UNTIMED)) {121 if (!CreateGui.getModel().netType().equals(NetType.UNTIMED)) {
122 if (inputArc == null)122 if (inputArc == null)
123 label.setText("");123 pnName.setText("");
124 else {124 else {
125 if (!CreateGui.getApp().showZeroToInfinityIntervals()) {125 if (!CreateGui.getApp().showZeroToInfinityIntervals()) {
126 if (inputArc.interval().toString(showConstantNames).equals("[0,inf)")){126 if (inputArc.interval().toString(showConstantNames).equals("[0,inf)")){
127 label.setText("");127 pnName.setText("");
128 }128 }
129 else {129 else {
130 label.setText(inputArc.interval().toString(showConstantNames));130 pnName.setText(inputArc.interval().toString(showConstantNames));
131 } 131 }
132 }132 }
133 else {133 else {
134 label.setText(inputArc.interval().toString(showConstantNames));134 pnName.setText(inputArc.interval().toString(showConstantNames));
135 }135 }
136 136
137 label.setText(getWeight().toString(showConstantNames)+" "+label.getText());137 pnName.setText(getWeight().toString(showConstantNames)+" "+pnName.getText());
138 138
139 // Handle constant highlighting139 // Handle constant highlighting
140 boolean focusedConstant = false;140 boolean focusedConstant = false;
@@ -154,9 +154,9 @@
154 }154 }
155 }155 }
156 if(focusedConstant){156 if(focusedConstant){
157 label.setForeground(Pipe.SELECTION_TEXT_COLOUR);157 pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
158 }else{158 }else{
159 label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);159 pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
160 }160 }
161 161
162 }162 }
@@ -169,8 +169,10 @@
169 /*label.setPosition((int) (myPath.midPoint.x + nameOffsetX)169 /*label.setPosition((int) (myPath.midPoint.x + nameOffsetX)
170 + label.getWidth() / 2 - 4, (int) (myPath.midPoint.y + nameOffsetY)170 + label.getWidth() / 2 - 4, (int) (myPath.midPoint.y + nameOffsetY)
171 - ((zoom / 55) * (zoom / 55)));*/171 - ((zoom / 55) * (zoom / 55)));*/
172 label.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))), 172
173 pnName.setPosition(Grid.getModifiedX((double) (myPath.midPoint.x + Zoomer.getZoomedValue(nameOffsetX, zoom))),
173 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));174 Grid.getModifiedY((double) (myPath.midPoint.y + Zoomer.getZoomedValue(nameOffsetY, zoom))));
175
174 }176 }
175177
176 public dk.aau.cs.model.tapn.TimedInputArc underlyingTimedInputArc() {178 public dk.aau.cs.model.tapn.TimedInputArc underlyingTimedInputArc() {
177179
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2019-03-16 13:57:33 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedOutputArcComponent.java 2019-05-09 09:07:50 +0000
@@ -133,8 +133,8 @@
133 }133 }
134134
135 public void updateLabel(boolean displayConstantNames) {135 public void updateLabel(boolean displayConstantNames) {
136 label.setText("");136 pnName.setText("");
137 label.setText(getWeight().toString(displayConstantNames)+" " + label.getText());137 pnName.setText(getWeight().toString(displayConstantNames)+" " + pnName.getText());
138 setLabelPosition();138 setLabelPosition();
139 }139 }
140140
141141
=== modified file 'src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java'
--- src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java 2019-01-27 12:49:43 +0000
+++ src/pipe/gui/graphicElements/tapn/TimedTransportArcComponent.java 2019-05-09 09:07:50 +0000
@@ -97,17 +97,19 @@
97 public void updateLabel(boolean displayConstantNames) {97 public void updateLabel(boolean displayConstantNames) {
98 if (isInPreSet && underlyingTransportArc != null) {98 if (isInPreSet && underlyingTransportArc != null) {
99 if (CreateGui.getApp().showZeroToInfinityIntervals()){99 if (CreateGui.getApp().showZeroToInfinityIntervals()){
100 label.setText(underlyingTransportArc.interval().toString(100 pnName.setText(underlyingTransportArc.interval().toString(
101 displayConstantNames)101 displayConstantNames)
102 + " : " + getGroup());102 + " : " + getGroup());
103 }103 }
104 else {104 else {
105 if (underlyingTransportArc.interval().toString(105 if (underlyingTransportArc.interval().toString(
106 displayConstantNames).equals("[0,inf)")) {106 displayConstantNames).equals("[0,inf)")) {
107 label.setText(" : " + String.valueOf(getGroup()));107
108 pnName.setText(" : " + String.valueOf(getGroup()));
109
108 }110 }
109 else {111 else {
110 label.setText(underlyingTransportArc.interval().toString(112 pnName.setText(underlyingTransportArc.interval().toString(
111 displayConstantNames)113 displayConstantNames)
112 + " : " + getGroup());114 + " : " + getGroup());
113 } 115 }
@@ -131,19 +133,19 @@
131 }133 }
132 }134 }
133 if(focusedConstant){135 if(focusedConstant){
134 label.setForeground(Pipe.SELECTION_TEXT_COLOUR);136 pnName.setForeground(Pipe.SELECTION_TEXT_COLOUR);
135 }else{137 }else{
136 label.setForeground(Pipe.ELEMENT_TEXT_COLOUR);138 pnName.setForeground(Pipe.ELEMENT_TEXT_COLOUR);
137 }139 }
138 140
139 } else if (!isInPreSet) {141 } else if (!isInPreSet) {
140 label.setText(" : " + String.valueOf(getGroup()));142 pnName.setText(" : " + String.valueOf(getGroup()));
141 } else {143 } else {
142 label.setText("");144 pnName.setText("");
143 }145 }
144 146
145 if(underlyingTransportArc != null){147 if(underlyingTransportArc != null){
146 label.setText(getWeight().toString(displayConstantNames)+" "+label.getText());148 pnName.setText(getWeight().toString(displayConstantNames)+" "+pnName.getText());
147 }149 }
148 150
149 this.setLabelPosition();151 this.setLabelPosition();

Subscribers

People subscribed via source and target branches