← Back to branch summary

~tapaal-developers/tapaal/fix-891944-delshared

« back to all changes in this revision

Viewing changes to src/pipe/gui/Animator.java

Merged branch fixing bug #940234 by Kenneth Yrke Jørgensen review by Kenneth Yrke Jørgensen approved by Mathias Andersen, Jiri Srba

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/Animator.java
250
250
 
251
251
        // TODO: Clean up this method
252
252
        public void fireTransition(TimedTransition transition) {
 
253
                
 
254
                CreateGui.getAnimationHistory().clearStepsForward();
 
255
                
253
256
                NetworkMarking next = null;
254
257
                try{
255
258
                        if (getFiringmode() != null) {
301
304
        }
302
305
 
303
306
        public boolean letTimePass(BigDecimal delay) {
 
307
                CreateGui.getAnimationHistory().clearStepsForward();
 
308
                
304
309
                boolean result = false;
305
310
                if (currentMarking().isDelayPossible(delay)) {
306
311
                        addMarking(new TAPNNetworkTimeDelayStep(delay), currentMarking().delay(delay));