Merge lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755 into lp:tapaal

Proposed by Peter Haahr Taankvist
Status: Merged
Approved by: Jiri Srba
Approved revision: 976
Merged at revision: 975
Proposed branch: lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755
Merge into: lp:tapaal
Diff against target: 29 lines (+4/-0)
2 files modified
src/pipe/gui/graphicElements/Place.java (+2/-0)
src/pipe/gui/graphicElements/Transition.java (+2/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Peter Haahr Taankvist (community) Needs Resubmitting
Review via email: mp+353011@code.launchpad.net

Description of the change

Names of transitions and places are now painted when the object is selected.

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

Deselecting does not work. To reproduce open Intro Example and start clicking on places and transitions and the names stay selected (blue) for over even when the actual place/transition
is not selected any more.

review: Needs Fixing
976. By Peter Taankvist <email address hidden>

Paint PNnames on select and undo paint on unselect

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

Added the line the right place. So now the text turns black when deselecting the object.

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
=== modified file 'src/pipe/gui/graphicElements/Place.java'
--- src/pipe/gui/graphicElements/Place.java 2018-05-13 14:57:15 +0000
+++ src/pipe/gui/graphicElements/Place.java 2018-08-14 07:53:04 +0000
@@ -108,8 +108,10 @@
108108
109 if (selected && !ignoreSelection) {109 if (selected && !ignoreSelection) {
110 g2.setColor(Pipe.SELECTION_FILL_COLOUR);110 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
111 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
111 } else {112 } else {
112 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);113 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
114 pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
113 }115 }
114 g2.fill(placeEllipse);116 g2.fill(placeEllipse);
115117
116118
=== modified file 'src/pipe/gui/graphicElements/Transition.java'
--- src/pipe/gui/graphicElements/Transition.java 2018-05-13 14:57:15 +0000
+++ src/pipe/gui/graphicElements/Transition.java 2018-08-14 07:53:04 +0000
@@ -98,8 +98,10 @@
9898
99 if (selected && !ignoreSelection) {99 if (selected && !ignoreSelection) {
100 g2.setColor(Pipe.SELECTION_FILL_COLOUR);100 g2.setColor(Pipe.SELECTION_FILL_COLOUR);
101 pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
101 } else {102 } else {
102 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);103 g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
104 pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
103 }105 }
104106
105 if (highlighted) {107 if (highlighted) {

Subscribers

People subscribed via source and target branches