← Back to branch summary

~yrke/tapaal/tapaal-fix-1756865

« back to all changes in this revision

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

  • Committer: Jiri Srba
  • Date: 2017-05-23 08:16:55 UTC
  • mfrom: (939.1.2 rapid-drawing)
  • Revision ID: srba.jiri@gmail.com-20170523081655-kvise51r0fm9cs75
merged in branch lp:~tapaal-contributor/tapaal/rapid-drawing-fix-810906
for fast drawing of place and transitions when ctl key is hold pressed

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/DrawingSurfaceImpl.java
1
1
package pipe.gui;
2
2
 
3
 
import java.awt.Component;
4
 
import java.awt.Container;
5
 
import java.awt.Cursor;
6
 
import java.awt.Dimension;
7
 
import java.awt.Graphics;
8
 
import java.awt.Graphics2D;
9
 
import java.awt.Point;
10
 
import java.awt.Rectangle;
 
3
import java.awt.*;
11
4
import java.awt.event.MouseEvent;
 
5
import java.awt.event.MouseListener;
12
6
import java.awt.event.MouseWheelEvent;
13
7
import java.awt.print.PageFormat;
14
8
import java.awt.print.Printable;
20
14
import javax.swing.JViewport;
21
15
import javax.swing.SwingUtilities;
22
16
import javax.swing.event.MouseInputAdapter;
 
17
 
23
18
import pipe.dataLayer.DataLayer;
24
19
import pipe.dataLayer.Template;
25
20
import pipe.gui.GuiFrame.GUIMode;
31
26
import pipe.gui.graphicElements.Place;
32
27
import pipe.gui.graphicElements.PlaceTransitionObject;
33
28
import pipe.gui.graphicElements.Transition;
34
 
import pipe.gui.graphicElements.tapn.TimedInputArcComponent;
35
 
import pipe.gui.graphicElements.tapn.TimedPlaceComponent;
36
 
import pipe.gui.graphicElements.tapn.TimedTransitionComponent;
37
 
import pipe.gui.graphicElements.tapn.TimedTransportArcComponent;
38
 
import pipe.gui.handler.AnimationHandler;
39
 
import pipe.gui.handler.AnnotationNoteHandler;
40
 
import pipe.gui.handler.ArcHandler;
41
 
import pipe.gui.handler.LabelHandler;
42
 
import pipe.gui.handler.PlaceHandler;
43
 
import pipe.gui.handler.TAPNTransitionHandler;
44
 
import pipe.gui.handler.TimedArcHandler;
45
 
import pipe.gui.handler.TransitionHandler;
46
 
import pipe.gui.handler.TransportArcHandler;
 
29
import pipe.gui.graphicElements.tapn.*;
 
30
import pipe.gui.handler.*;
47
31
import pipe.gui.undo.AddPetriNetObjectEdit;
48
32
import pipe.gui.undo.AddTimedPlaceCommand;
49
33
import pipe.gui.undo.AddTimedTransitionCommand;
59
43
public class DrawingSurfaceImpl extends JLayeredPane implements Observer,
60
44
Printable, DrawingSurface {
61
45
        private static final long serialVersionUID = 4434596266503933386L;
62
 
 
63
46
        private boolean netChanged = false;
64
 
 
65
47
        private boolean animationmode = false;
66
48
 
67
49
        public Arc createArc; // no longer static
618
600
                @Override
619
601
                public void mousePressed(MouseEvent e) {
620
602
                        if(app.getGUIMode().equals(GUIMode.animation)) return;
621
 
                        
 
603
 
 
604
                        // check for control down here enables it to attach the arc being drawn to an existing place/transition
 
605
 
622
606
                        Point start = e.getPoint();
623
607
                        Point p;
624
608
                        if (SwingUtilities.isLeftMouseButton(e)) {
 
609
 
625
610
                                Pipe.ElementType mode = app.getMode();
626
611
                                switch (mode) {
627
612
                                case PLACE:
635
620
                                        break;
636
621
 
637
622
                                case TAPNPLACE:
 
623
                                        // create place
638
624
                                        PlaceTransitionObject pto2 = newTimedPlace(e.getPoint());
639
625
                                        getUndoManager().addNewEdit(
640
626
                                                        new AddTimedPlaceCommand(
641
627
                                                                        (TimedPlaceComponent) pto2, model,
642
628
                                                                        guiModel, view));
643
629
                                        if (e.isControlDown()) {
 
630
                                                // connect arc
 
631
                                                app.setMode(ElementType.TAPNARC);
 
632
                                                getPlaceTransitionObjectHandlerOf(pto2).mousePressed(e);
 
633
                                                getPlaceTransitionObjectHandlerOf(pto2).mouseReleased(e);
644
634
                                                app.setFastMode(ElementType.FAST_TRANSITION);
 
635
                                                // enter fast mode
645
636
                                                pnObject.dispatchEvent(e);
646
637
                                        }
647
638
                                        break;
658
649
                                        }
659
650
                                        break;
660
651
                                case TAPNTRANS:
 
652
                                        // create transition
661
653
                                        pto = newTAPNTransition(e.getPoint());
662
654
                                        getUndoManager().addNewEdit(
663
655
                                                        new AddTimedTransitionCommand(
664
656
                                                                        (TimedTransitionComponent) pto, model,
665
657
                                                                        guiModel, view));
666
658
                                        if (e.isControlDown()) {
 
659
                                                // connect arc
 
660
                                                app.setMode(ElementType.TAPNARC);
 
661
                                                getPlaceTransitionObjectHandlerOf(pto).mousePressed(e);
 
662
                                                getPlaceTransitionObjectHandlerOf(pto).mouseReleased(e);
 
663
                                                // enter fast mode
667
664
                                                app.setFastMode(ElementType.FAST_PLACE);
668
665
                                                pnObject.dispatchEvent(e);
669
666
                                        }
705
702
                                        dragStart = new Point(start);
706
703
                                        break;
707
704
 
 
705
                                case FAST_TRANSITION:
 
706
                                        // create transition
 
707
                                        pto = newTAPNTransition(e.getPoint());
 
708
                                        getUndoManager().addNewEdit(new AddTimedTransitionCommand((TimedTransitionComponent) pto, model, guiModel, view));
 
709
                                        app.setMode(ElementType.TAPNARC);
 
710
                                        getPlaceTransitionObjectHandlerOf(pto).mouseReleased(e);
 
711
 
 
712
                                        if (e.isControlDown()) {
 
713
                                                // connect arc
 
714
                                                pnObject.dispatchEvent(e);
 
715
                                                app.setMode(ElementType.TAPNARC);
 
716
                                                getPlaceTransitionObjectHandlerOf(pto).mousePressed(e);
 
717
                                                getPlaceTransitionObjectHandlerOf(pto).mouseReleased(e);
 
718
                                                // enter fast mode
 
719
                                                app.setFastMode(ElementType.FAST_PLACE);
 
720
                                        } else{
 
721
                                                app.endFastMode();
 
722
                                        }
 
723
                                        break;
 
724
                                case FAST_PLACE:
 
725
                                        // create place
 
726
                                        PlaceTransitionObject pto3 = newTimedPlace(e.getPoint());
 
727
                                        getUndoManager().addNewEdit(new AddTimedPlaceCommand((TimedPlaceComponent) pto3, model, guiModel, view));
 
728
                                        app.setMode(ElementType.TAPNARC);
 
729
                                        getPlaceTransitionObjectHandlerOf(pto3).mouseReleased(e);
 
730
 
 
731
                                        if (e.isControlDown()) {
 
732
                                                // connect arc
 
733
                                                pnObject.dispatchEvent(e);
 
734
                                                app.setMode(ElementType.TAPNARC);
 
735
                                                getPlaceTransitionObjectHandlerOf(pto3).mousePressed(e);
 
736
                                                getPlaceTransitionObjectHandlerOf(pto3).mouseReleased(e);
 
737
                                                // enter fast mode
 
738
                                                app.setFastMode(ElementType.FAST_TRANSITION);
 
739
                                        } else{
 
740
                                                app.endFastMode();
 
741
                                        }
 
742
                                        break;
708
743
                                default:
709
744
                                        break;
710
745
                                }
715
750
                        updatePreferredSize();
716
751
                }
717
752
 
 
753
                private MouseListener getPlaceTransitionObjectHandlerOf(PlaceTransitionObject obj){
 
754
                        for (MouseListener listener : obj.getMouseListeners()) {
 
755
                                if (listener instanceof PlaceTransitionObjectHandler)
 
756
                                        return listener;
 
757
                        }
 
758
                        return null;
 
759
                }
 
760
 
718
761
                private void addPoint(final Arc createArc, final MouseEvent e) {
719
762
                        int x = Grid.getModifiedX(e.getX());
720
763
                        int y = Grid.getModifiedY(e.getY());