TAPAAL

Merge lp:~tapaal-contributor/tapaal/notes-hides-namelabels-1848947 into lp:tapaal

  1. notes-hides-namelabels-1848947
  2. Merge into trunk
Proposed by Peter Haahr Taankvist
Status: Merged
Approved by: Jiri Srba
Approved revision: 1021
Merged at revision: 1025
Proposed branch: lp:~tapaal-contributor/tapaal/notes-hides-namelabels-1848947
Merge into: lp:tapaal
Diff against target: 55 lines (+8/-0)
4 files modified
src/pipe/gui/Pipe.java (+1/-0)
src/pipe/gui/graphicElements/Arc.java (+1/-0)
src/pipe/gui/graphicElements/NameLabel.java (+4/-0)
src/pipe/gui/graphicElements/PetriNetObject.java (+2/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/notes-hides-namelabels-1848947
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Peter Haahr Taankvist (community) Needs Resubmitting
Review via email: mp+374604@code.launchpad.net

Commit message

Namelabels are no longer hidden under annotation notes

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

The notes hide also intervals on arcs, so this should be fixed in this branch as well.

review: Needs Fixing
lp:~tapaal-contributor/tapaal/notes-hides-namelabels-1848947 updated
1021. By Peter Taankvist <email address hidden>

Add layering to arc label too

Revision history for this message
Peter Haahr Taankvist (ptaank) wrote :

Added the layering to arc labels too.

review: Needs Resubmitting
Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/pipe/gui/Pipe.java'
2--- src/pipe/gui/Pipe.java 2019-03-28 14:25:10 +0000
3+++ src/pipe/gui/Pipe.java 2019-10-31 16:29:14 +0000
4@@ -42,6 +42,7 @@
5 public static final int PLACE_TRANSITION_LAYER_OFFSET = 30;
6 public static final int NOTE_LAYER_OFFSET = 10;
7 public static final int SELECTION_LAYER_OFFSET = 90;
8+ public static final int NAMELABEL_LAYER_OFFSET = 15;
9 public static final int LOWEST_LAYER_OFFSET = 0;
10
11 // For AnnotationNote appearance:
12
13=== modified file 'src/pipe/gui/graphicElements/Arc.java'
14--- src/pipe/gui/graphicElements/Arc.java 2019-09-09 14:52:47 +0000
15+++ src/pipe/gui/graphicElements/Arc.java 2019-10-31 16:29:14 +0000
16@@ -359,6 +359,7 @@
17
18 updateArcPosition();
19 if (getParent() != null && pnName.getParent() == null) {
20+ getParent().setLayer(pnName, JLayeredPane.DEFAULT_LAYER + pnName.getLayerOffset());
21 getParent().add(pnName);
22 }
23 }
24
25=== modified file 'src/pipe/gui/graphicElements/NameLabel.java'
26--- src/pipe/gui/graphicElements/NameLabel.java 2019-03-18 17:44:30 +0000
27+++ src/pipe/gui/graphicElements/NameLabel.java 2019-10-31 16:29:14 +0000
28@@ -113,4 +113,8 @@
29 super.setText(text);
30 }
31 }
32+
33+ public int getLayerOffset() {
34+ return Pipe.NAMELABEL_LAYER_OFFSET;
35+ }
36 }
37
38=== modified file 'src/pipe/gui/graphicElements/PetriNetObject.java'
39--- src/pipe/gui/graphicElements/PetriNetObject.java 2019-10-28 18:57:53 +0000
40+++ src/pipe/gui/graphicElements/PetriNetObject.java 2019-10-31 16:29:14 +0000
41@@ -8,6 +8,7 @@
42 import java.util.EventListener;
43
44 import javax.swing.JComponent;
45+import javax.swing.JLayeredPane;
46
47 import dk.aau.cs.debug.Logger;
48 import pipe.dataLayer.DataLayer;
49@@ -224,6 +225,7 @@
50 public void addLabelToContainer() {
51 if (getParent() != null && pnName.getParent() == null) {
52 getParent().add(pnName);
53+ getParent().setLayer(pnName, JLayeredPane.DEFAULT_LAYER + pnName.getLayerOffset());
54 }
55 }
56

Subscribers

People subscribed via source and target branches