← Back to branch summary

~tapaal-contributor/tapaal/save-as-fix-1648076

« back to all changes in this revision

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

merged in branch fixing enabled-transition-in-editor-fix-1641313
that also changes the future enabled transitions from blue to yellow

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/AnimationHistoryComponent.java
5
5
import java.awt.event.MouseMotionListener;
6
6
 
7
7
import javax.swing.DefaultListModel;
8
 
import javax.swing.JLabel;
9
8
import javax.swing.JList;
10
9
import javax.swing.ListSelectionModel;
11
10
 
12
11
import pipe.dataLayer.Template;
13
12
import pipe.gui.graphicElements.Transition;
14
13
 
15
 
import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
16
 
import dk.aau.cs.model.tapn.simulation.TimedTAPNNetworkTrace;
17
14
import dk.aau.cs.verification.VerifyTAPN.TraceType;
18
15
 
19
16
public class AnimationHistoryComponent extends JList {
24
21
                super();
25
22
                setModel(new DefaultListModel());
26
23
                setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
27
 
                reset();
28
24
                
29
25
                for (MouseListener listener : getMouseListeners()) {
30
26
                        removeMouseListener(listener);
165
161
                }
166
162
                for (Template t : CreateGui.getCurrentTab().activeTemplates()){
167
163
                        for(Transition trans : t.guiModel().getTransitions()){
168
 
                                if(trans.isEnabled(true) || trans.isBlueTransition(true)){
 
164
                                if(trans.isEnabled(true) || trans.isDelayEnabledTransition(true)){
169
165
                                        return;
170
166
                                }
171
167
                        }