Remove decorator of empty label.

Needs kieler/KLighD#139 to work. Signed-off-by: Soeren Domroes <[email protected]>
kieler · Aug 22, 2022 · 0618e6c · 0618e6c
1 parent 98eb8a4
commit 0618e6c
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/....ui/src/de/cau/cs/kieler/sccharts/ui/synthesis/labels/TransitionPriorityLabelManager.java b/....ui/src/de/cau/cs/kieler/sccharts/ui/synthesis/labels/TransitionPriorityLabelManager.java
@@ -24,6 +24,7 @@
 import de.cau.cs.kieler.klighd.kgraph.KLabel;
 import de.cau.cs.kieler.klighd.krendering.KRendering;
 import de.cau.cs.kieler.klighd.krendering.KRenderingRef;
+import de.cau.cs.kieler.klighd.labels.decoration.LabelDecorationConfigurator;
 import de.cau.cs.kieler.klighd.labels.management.AbstractKlighdLabelManager;
 import de.cau.cs.kieler.sccharts.Transition;
 
@@ -67,7 +68,9 @@ public Result doResizeLabel(ElkLabel label, double targetWidth) {
                         // The new label is the priority followed by a period
                         return Result.modified(matcher.group(1) + ".");
                     } else {
-                        // If no priority available 
+                        // If no priority available
+                        kLabel.setText("");
+                        LabelDecorationConfigurator.create().applyTo(kLabel);
                         return Result.modified("");
                     }
                 }