← Back to branch summary

~yrke/tapaal/remove-staticIgnoreSelect

« back to all changes in this revision

Viewing changes to src/pipe/gui/graphicElements/Transition.java

  • Committer: Jiri Srba
  • Date: 2018-08-14 13:06:51 UTC
  • mfrom: (974.1.2 tapaal)
  • Revision ID: srba@cs.aau.dk-20180814130651-e18hqqau9axoml3i
merged in branch lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755
that highlights names of selected places and transitions

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/graphicElements/Transition.java
98
98
 
99
99
                if (selected && !ignoreSelection) {
100
100
                        g2.setColor(Pipe.SELECTION_FILL_COLOUR);
 
101
                        pnName.setForeground(Pipe.SELECTION_LINE_COLOUR);
101
102
                } else {
102
103
                        g2.setColor(Pipe.ELEMENT_FILL_COLOUR);
 
104
                        pnName.setForeground(Pipe.ELEMENT_LINE_COLOUR);
103
105
                }
104
106
 
105
107
                if (highlighted) {