Merge lp:~yrke/tapaal/fix1883971-save-arcpath-point-coords-error into lp:tapaal

Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1062
Merged at revision: 1063
Proposed branch: lp:~yrke/tapaal/fix1883971-save-arcpath-point-coords-error
Merge into: lp:tapaal
Diff against target: 57 lines (+10/-11)
2 files modified
src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java (+5/-5)
src/pipe/gui/graphicElements/ArcPath.java (+5/-6)
To merge this branch: bzr merge lp:~yrke/tapaal/fix1883971-save-arcpath-point-coords-error
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+385983@code.launchpad.net
To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

It is more convenient if the branch is first named by the intuitive description and the bug id at last.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java'
2--- src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-05-25 19:02:55 +0000
3+++ src/dk/aau/cs/io/TimedArcPetriNetNetworkWriter.java 2020-06-18 08:41:54 +0000
4@@ -59,7 +59,7 @@
5 public TimedArcPetriNetNetworkWriter(
6 TimedArcPetriNetNetwork network,
7 Iterable<Template> templates,
8- Iterable<TAPNQuery> queries,
9+ Iterable<TAPNQuery> queries,
10 Iterable<Constant> constants) {
11 this.network = network;
12 this.templates = templates;
13@@ -363,8 +363,8 @@
14
15 Element placeElement = document.createElement("place");
16
17- placeElement.setAttribute("positionX", String.valueOf(inputPlace.getPositionX()));
18- placeElement.setAttribute("positionY", String.valueOf(inputPlace.getPositionY()));
19+ placeElement.setAttribute("positionX", String.valueOf(inputPlace.getOriginalX()));
20+ placeElement.setAttribute("positionY", String.valueOf(inputPlace.getOriginalY()));
21 placeElement.setAttribute("name", inputPlace.underlyingPlace().name());
22 placeElement.setAttribute("displayName", (inputPlace.getAttributesVisible() ? "true" : "false"));
23 placeElement.setAttribute("id", (inputPlace.getId() != null ? inputPlace.getId() : "error"));
24@@ -401,8 +401,8 @@
25
26 Element transitionElement = document.createElement("transition");
27
28- transitionElement.setAttribute("positionX", String.valueOf(inputTransition.getPositionX()));
29- transitionElement.setAttribute("positionY", String.valueOf(inputTransition.getPositionY()));
30+ transitionElement.setAttribute("positionX", String.valueOf(inputTransition.getOriginalX()));
31+ transitionElement.setAttribute("positionY", String.valueOf(inputTransition.getOriginalY()));
32 transitionElement.setAttribute("nameOffsetX", String.valueOf(inputTransition.getNameOffsetX()));
33 transitionElement.setAttribute("nameOffsetY", String.valueOf(inputTransition.getNameOffsetY()));
34 transitionElement.setAttribute("name", inputTransition.underlyingTransition().name());
35
36=== modified file 'src/pipe/gui/graphicElements/ArcPath.java'
37--- src/pipe/gui/graphicElements/ArcPath.java 2020-04-30 12:57:50 +0000
38+++ src/pipe/gui/graphicElements/ArcPath.java 2020-06-18 08:41:54 +0000
39@@ -569,13 +569,12 @@
40 int length = getEndIndex() + 1;
41 String[][] details = new String[length][3];
42
43- int zoom = this.getArc().getZoom();
44- int x, y;
45+ int x, y;
46 for (int c = 0; c < length; c++) {
47- x = (pathPoints.get(c)).getX();
48- details[c][0] = String.valueOf(Zoomer.getUnzoomedValue(x, zoom));
49- y = (pathPoints.get(c)).getY();
50- details[c][1] = String.valueOf(Zoomer.getUnzoomedValue(y, zoom));
51+ x = (pathPoints.get(c)).getOriginalX();
52+ details[c][0] = String.valueOf(x);
53+ y = (pathPoints.get(c)).getOriginalY();
54+ details[c][1] = String.valueOf(y);
55 details[c][2] = String.valueOf((pathPoints.get(c)).getPointType());
56 }
57 return details;

Subscribers

People subscribed via source and target branches