Constants not blinking - fix 1895130 (#146)

Fixes: https://bugs.launchpad.net/tapaal/+bug/1895130
TAPAAL · Apr 19, 2024 · e8237bf · e8237bf
2 parents 1f687ce + a033098
commit e8237bf
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/main/java/pipe/gui/petrinet/graphicElements/tapn/TimedInputArcComponent.java b/src/main/java/pipe/gui/petrinet/graphicElements/tapn/TimedInputArcComponent.java
@@ -142,6 +142,8 @@ public void updateLabel(boolean showConstantNames) {
                 if(((ConstantWeight) getWeight()).constant().hasFocus()){
                     focusedConstant = true;
                 }
+
+                isvisible = ((ConstantWeight) getWeight()).constant().getVisible();
                 /*if(((ConstantWeight) getWeight()).constant().getVisible()){
                     focusedConstant = false;
                 }*/

diff --git a/src/main/java/pipe/gui/petrinet/graphicElements/tapn/TimedOutputArcComponent.java b/src/main/java/pipe/gui/petrinet/graphicElements/tapn/TimedOutputArcComponent.java
@@ -104,6 +104,8 @@ public void updateLabel(boolean displayConstantNames) {
             if(((ConstantWeight) getWeight()).constant().hasFocus()){
                 focusedConstant = true;
             }
+
+			isvisible = ((ConstantWeight) getWeight()).constant().getVisible();
         }
         if (focusedConstant) {
             getNameLabel().setForeground(Constants.SELECTION_TEXT_COLOUR);