← Back to branch summary

~tapaal-contributor/tapaal/unselect-objects-after-undo-1894108

« back to all changes in this revision

Viewing changes to src/dk/aau/cs/gui/components/EnabledTransitionsList.java

  • Committer: srba.jiri at gmail
  • Date: 2020-08-19 12:02:28 UTC
  • mfrom: (1071.2.34 untimed-timed-gui)
  • Revision ID: srba.jiri@gmail.com-20200819120228-ktxdev3ou3kuj3l0
merged in lp:~tapaal-contributor/tapaal/untimed-timed-gui adding timed/untimed lens projection

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/dk/aau/cs/gui/components/EnabledTransitionsList.java
20
20
import org.jetbrains.annotations.NotNull;
21
21
import pipe.dataLayer.Template;
22
22
import pipe.gui.CreateGui;
 
23
import pipe.gui.SimulationControl;
23
24
import pipe.gui.graphicElements.Transition;
24
25
import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
25
26
//TODO clean up!!! 
63
64
        }
64
65
 
65
66
        public void reInitDone(){
66
 
                if(CreateGui.getCurrentTab().getDelayEnabledTransitionControl().isRandomTransitionMode()){
 
67
                if(SimulationControl.getInstance().isRandomTransitionMode()){
67
68
                        selectRandom();
68
69
                        return;
69
70
                }
125
126
 
126
127
                public String toString(boolean showIntervals) {
127
128
 
128
 
                        String interval = transition.getDInterval() == null || !showIntervals ? "" : transition.getDInterval().toString() + " ";
 
129
                        String interval = transition.getDInterval() == null || !showIntervals || !transition.isTimed() ? "" : transition.getDInterval().toString() + " ";
129
130
                        
130
131
                        String transitionName = getTransition().getName(); 
131
132
                        if(isShared()){