← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/PetriNetObject.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/PetriNetObject.java
3
3
import java.awt.Graphics;
4
4
import java.awt.Rectangle;
5
5
import java.awt.event.*;
 
6
 
 
7
import dk.aau.cs.gui.TabContent;
6
8
import pipe.dataLayer.DataLayer;
7
9
import pipe.gui.canvas.DrawingSurfaceImpl;
8
10
import pipe.gui.Pipe;
19
21
        /** x/y position position on screen (zoomed) */
20
22
        protected int positionX;
21
23
        protected int positionY;
 
24
        protected TabContent.TAPNLens lens = TabContent.TAPNLens.Default;
22
25
 
23
26
        // The x/y coordinate of object at 100% zoom.
24
27
        //XXX: pushed down from PlaceTransitionObject and consolidated from note, need further refactoring and rename, //kyrke 2019-08-23
285
288
                return positionY;
286
289
        }
287
290
 
 
291
        public boolean isTimed(){
 
292
            return lens.isTimed();
 
293
    }
 
294
 
 
295
    public void setLens(TabContent.TAPNLens lens){
 
296
            this.lens = lens;
 
297
    }
 
298
 
288
299
    @Override
289
300
    public GraphicalElement getGraphicalElement() {
290
301
        return this;