← Back to branch summary

~tapaal-developers/tapaal/trunk

« back to all changes in this revision

Viewing changes to src/pipe/gui/handler/LabelHandler.java

  • Committer: Jiri Srba
  • Date: 2019-03-27 20:55:09 UTC
  • mfrom: (1000.1.1 tapaal)
  • Revision ID: srba@cs.aau.dk-20190327205509-vi4y8bj054twq33v
merged in branch  lp:~tapaal-contributor/tapaal/double-click-on-arcs-to-edit-1820017 that allows to enter arc dialog by double clicking on a label

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/handler/LabelHandler.java
3
3
import java.awt.Point;
4
4
import java.awt.event.MouseEvent;
5
5
import java.awt.event.MouseWheelEvent;
6
 
 
7
6
import javax.swing.SwingUtilities;
8
 
 
 
7
import pipe.dataLayer.NetType;
9
8
import pipe.gui.CreateGui;
 
9
import pipe.gui.graphicElements.Arc;
10
10
import pipe.gui.graphicElements.NameLabel;
11
11
import pipe.gui.graphicElements.PetriNetObject;
 
12
import pipe.gui.graphicElements.tapn.TimedOutputArcComponent;
12
13
 
13
14
public class LabelHandler extends javax.swing.event.MouseInputAdapter implements
14
15
                java.awt.event.MouseWheelListener {
31
32
 
32
33
        @Override
33
34
        public void mousePressed(MouseEvent e) {
 
35
                if(obj instanceof Arc) {
 
36
                        if (((Arc) obj).isPrototype()) {
 
37
                                return;
 
38
                        }
 
39
        
 
40
                        if (CreateGui.getApp().isEditionAllowed()) {
 
41
                                if (e.getClickCount() == 2) {
 
42
                                        Arc arc = (Arc) obj;
 
43
                                        if (!CreateGui.getModel().netType().equals(NetType.UNTIMED)) {
 
44
                                                ((TimedOutputArcComponent) arc).showTimeIntervalEditor();
 
45
                                        }
 
46
                                }
 
47
                        }
 
48
                }
34
49
                dragInit = e.getPoint(); //
35
50
                // dragInit = e.getLocationOnScreen(); //causes exception in Windows!
36
51
                dragInit = javax.swing.SwingUtilities.convertPoint(nl, dragInit, obj);
60
75
        public void mouseWheelMoved(MouseWheelEvent e) {
61
76
                obj.dispatchEvent(e);
62
77
        }
63
 
 
64
78
}