← Back to branch summary

~tapaal-contributor/tapaal/fix-1894106-LabelsWithConstantsAreNotShown

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/tapn/TimedPlaceComponent.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/TimedPlaceComponent.java
23
23
import javax.swing.BoxLayout;
24
24
import javax.swing.JTextArea;
25
25
 
 
26
import dk.aau.cs.gui.TabContent;
26
27
import pipe.gui.CreateGui;
27
28
import pipe.gui.Pipe;
28
29
import pipe.gui.graphicElements.Place;
49
50
        private Window ageOfTokensWindow = new Window(new Frame());
50
51
        private final Shape dashedOutline = createDashedOutline();
51
52
 
52
 
        public TimedPlaceComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedPlace place) {
 
53
        public TimedPlaceComponent(int positionXInput, int positionYInput, dk.aau.cs.model.tapn.TimedPlace place, TabContent.TAPNLens lens) {
53
54
                super(positionXInput, positionYInput);
54
55
                this.place = place;
55
56
        this.place.addTimedPlaceListener(listener);
56
 
 
 
57
        this.lens = lens;
57
58
                attributesVisible = true;
58
59
 
59
60
    }
63
64
        int positionYInput,
64
65
        String idInput,
65
66
        int nameOffsetXInput,
66
 
        int nameOffsetYInput
 
67
        int nameOffsetYInput,
 
68
        TabContent.TAPNLens lens
67
69
    ) {
68
70
 
69
71
                super(positionXInput, positionYInput, idInput, nameOffsetXInput, nameOffsetYInput);
70
72
        attributesVisible = true;
 
73
        this.lens = lens;
71
74
 
72
75
    }
73
76
 
74
 
        @Override
 
77
    @Override
75
78
        protected void addMouseHandler() {
76
79
                //XXX: kyrke 2018-09-06, this is bad as we leak "this", think its ok for now, as it alwas constructed when
77
80
                //XXX: handler is called. Make static constructor and add handler from there, to make it safe.
173
176
                                }
174
177
                        }
175
178
        }
176
 
 
 
179
        if(!lens.isTimed()){
 
180
            drawDots = (marking > 0 && marking < 6);
 
181
        }
177
182
        // structure sees how many markings there are and fills the place in
178
183
        // with the appropriate number or tokens.
179
184
        if(drawDots) {
277
282
                }
278
283
                
279
284
                // Build interface
280
 
                if (show) {
 
285
                if (show && isTimed()) {
281
286
                        ageOfTokensWindow = new Window(new Frame());
282
287
                        ageOfTokensWindow.add(new JTextArea(getStringOfTokens()));
283
288
                        ageOfTokensWindow.getComponent(0).setBackground(Color.lightGray);
410
415
        }
411
416
 
412
417
        public TimedPlaceComponent copy(TimedArcPetriNet tapn) {
413
 
                TimedPlaceComponent placeComponent = new TimedPlaceComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY());
 
418
                TimedPlaceComponent placeComponent = new TimedPlaceComponent(getOriginalX(), getOriginalY(), id, getNameOffsetX(), getNameOffsetY(), lens);
414
419
                placeComponent.setUnderlyingPlace(tapn.getPlaceByName(place.name()));
415
420
 
416
421
                return placeComponent;