Merge lp:~yrke/tapaal/fix-940234-clearfiringhistory into lp:tapaal

Proposed by Kenneth Yrke Jørgensen
Status: Merged
Approved by: Kenneth Yrke Jørgensen
Approved revision: 663
Merged at revision: 664
Proposed branch: lp:~yrke/tapaal/fix-940234-clearfiringhistory
Merge into: lp:tapaal
Diff against target: 46 lines (+5/-2)
3 files modified
src/pipe/gui/AnimationController.java (+0/-1)
src/pipe/gui/Animator.java (+5/-0)
src/pipe/gui/handler/AnimationHandler.java (+0/-1)
To merge this branch: bzr merge lp:~yrke/tapaal/fix-940234-clearfiringhistory
Reviewer Review Type Date Requested Status
Mathias Andersen (community) Approve
Jiri Srba Approve
Review via email: mp+94527@code.launchpad.net

Commit message

Merged branch fixing bug #940234

Description of the change

Merged bugfix branch

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve
Revision history for this message
Mathias Andersen (mande09) :
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/AnimationController.java'
2--- src/pipe/gui/AnimationController.java 2012-02-10 09:45:16 +0000
3+++ src/pipe/gui/AnimationController.java 2012-02-24 11:56:23 +0000
4@@ -347,7 +347,6 @@
5
6 switch (typeID) {
7 case TIMEPASS:
8- animBox.clearStepsForward();
9 CreateGui.getAnimator().letTimePass(
10 new BigDecimal(1, new MathContext(Pipe.AGE_PRECISION)));
11
12
13=== modified file 'src/pipe/gui/Animator.java'
14--- src/pipe/gui/Animator.java 2012-02-21 14:05:56 +0000
15+++ src/pipe/gui/Animator.java 2012-02-24 11:56:23 +0000
16@@ -250,6 +250,9 @@
17
18 // TODO: Clean up this method
19 public void fireTransition(TimedTransition transition) {
20+
21+ CreateGui.getAnimationHistory().clearStepsForward();
22+
23 NetworkMarking next = null;
24 try{
25 if (getFiringmode() != null) {
26@@ -301,6 +304,8 @@
27 }
28
29 public boolean letTimePass(BigDecimal delay) {
30+ CreateGui.getAnimationHistory().clearStepsForward();
31+
32 boolean result = false;
33 if (currentMarking().isDelayPossible(delay)) {
34 addMarking(new TAPNNetworkTimeDelayStep(delay), currentMarking().delay(delay));
35
36=== modified file 'src/pipe/gui/handler/AnimationHandler.java'
37--- src/pipe/gui/handler/AnimationHandler.java 2011-09-22 12:58:03 +0000
38+++ src/pipe/gui/handler/AnimationHandler.java 2012-02-24 11:56:23 +0000
39@@ -30,7 +30,6 @@
40
41 if (SwingUtilities.isLeftMouseButton(e) && transition.isEnabled()) {
42
43- CreateGui.getAnimationHistory().clearStepsForward();
44 CreateGui.getAnimator().fireTransition(transition);
45 CreateGui.getApp().setRandomAnimationMode(false);
46 }

Subscribers

People subscribed via source and target branches