← Back to branch summary

~tapaal-contributor/tapaal/disable-workflow-analysis-1896319

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/tapn/TimedInputArcComponent.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/pipe/gui/graphicElements/tapn/TimedInputArcComponent.java
2
2
 
3
3
import java.util.Hashtable;
4
4
 
 
5
import dk.aau.cs.gui.TabContent;
5
6
import pipe.gui.CreateGui;
6
7
import pipe.gui.Pipe;
7
8
import pipe.gui.graphicElements.PlaceTransitionObject;
24
25
                updateLabel(true);
25
26
        }
26
27
 
27
 
        public TimedInputArcComponent(PlaceTransitionObject source, PlaceTransitionObject target, TimedInputArc modelArc){
 
28
        public TimedInputArcComponent(PlaceTransitionObject source, PlaceTransitionObject target, TimedInputArc modelArc, TabContent.TAPNLens lens){
28
29
            super(source);
29
30
            setTarget(target);
30
31
            setUnderlyingArc(modelArc);
31
32
            updateLabel(true);
 
33
            this.lens = lens;
32
34
            sealArc();
33
35
    }
34
36
 
37
39
                updateLabel(true);
38
40
        }
39
41
 
 
42
    public TimedInputArcComponent(TimedOutputArcComponent arc, TabContent.TAPNLens lens) {
 
43
        super(arc);
 
44
        updateLabel(true);
 
45
        this.lens = lens;
 
46
    }
 
47
 
40
48
    @Override
41
49
        protected void addMouseHandler() {
42
50
                //XXX: kyrke 2018-09-06, this is bad as we leak "this", think its ok for now, as it alwas constructed when
82
90
        if (inputArc == null)
83
91
            getNameLabel().setText("");
84
92
        else {
85
 
            if (!CreateGui.getApp().showZeroToInfinityIntervals()) {
 
93
            if (!CreateGui.getApp().showZeroToInfinityIntervals() || !lens.isTimed()) {
86
94
                if (inputArc.interval().toString(showConstantNames).equals("[0,inf)")){
87
95
                    getNameLabel().setText("");
88
96
                }