From 04cec85f90b69eb0e59a7ed7a7463bd2b07c675c Mon Sep 17 00:00:00 2001 From: rensink Date: Sun, 4 Aug 2024 09:45:13 +0200 Subject: [PATCH] Correct count of label occurrences --- .../groove/gui/jgraph/AspectJEdge.java | 8 -- .../groove/gui/jgraph/AspectJVertex.java | 23 ++++ .../nl/utwente/groove/gui/jgraph/JCell.java | 7 ++ .../utwente/groove/gui/tree/LabelFilter.java | 100 ++++++++++++++---- .../nl/utwente/groove/gui/tree/LabelTree.java | 5 +- .../utwente/groove/gui/tree/TypeFilter.java | 7 +- 6 files changed, 119 insertions(+), 31 deletions(-) diff --git a/src/main/java/nl/utwente/groove/gui/jgraph/AspectJEdge.java b/src/main/java/nl/utwente/groove/gui/jgraph/AspectJEdge.java index 186a7056b..7394b2699 100644 --- a/src/main/java/nl/utwente/groove/gui/jgraph/AspectJEdge.java +++ b/src/main/java/nl/utwente/groove/gui/jgraph/AspectJEdge.java @@ -8,7 +8,6 @@ import java.util.Collections; import java.util.Comparator; import java.util.EnumSet; -import java.util.HashSet; import java.util.Set; import org.eclipse.jdt.annotation.NonNull; @@ -196,13 +195,6 @@ public Collection getKeys() { if (this.aspects.containsKey(Category.NESTING)) { return Collections.emptySet(); } else { - Set