Bug fix in 6.9.1 (label filter wasn't working correctly for LTS)

nl-utwente-groove · Aug 1, 2024 · bb47fe8 · bb47fe8
1 parent 7264f15
commit bb47fe8
Show file tree

Hide file tree

Showing 10 changed files with 86 additions and 70 deletions.
diff --git a/release/include/CHANGES.md b/release/include/CHANGES.md
@@ -3,6 +3,10 @@ GROOVE Change Log
 
 This document describes the major changes in the GROOVE tool set
 
+Release 6.9.2, 1 August 2024
+-------------------------------
+- Bug fix release (don't use 6.9.1)
+
 Release 6.9.1, 1 August 2024
 -------------------------------
 - Hugely improved behaviour of (label and) type tree (gh issue #786)

diff --git a/src/main/java/nl/utwente/groove/grammar/type/TypeLabel.java b/src/main/java/nl/utwente/groove/grammar/type/TypeLabel.java
@@ -30,6 +30,7 @@
 import nl.utwente.groove.graph.EdgeRole;
 import nl.utwente.groove.graph.Label;
 import nl.utwente.groove.io.HTMLConverter;
+import nl.utwente.groove.io.Util;
 import nl.utwente.groove.util.line.Line;
 import nl.utwente.groove.util.line.Line.Style;
 import nl.utwente.groove.util.parse.FormatException;
@@ -223,8 +224,11 @@ static public String toHtmlString(Label label) {
         }
     }
 
+    /** Text of the node type label in an untyped setting. */
+    static public final String NODE_LABEL_TEXT = "" + Util.UC_OMEGA;
+
     /** Type label for nodes in an untyped setting. */
-    static public final TypeLabel NODE = new TypeLabel("\u03A9", EdgeRole.NODE_TYPE);
+    static public final TypeLabel NODE = new TypeLabel(NODE_LABEL_TEXT, EdgeRole.NODE_TYPE);
 
     /**
      * Unique type factory used for creating labels statically.

diff --git a/src/main/java/nl/utwente/groove/gui/action/FindReplaceAction.java b/src/main/java/nl/utwente/groove/gui/action/FindReplaceAction.java
@@ -40,7 +40,7 @@
 import nl.utwente.groove.gui.jgraph.JGraph;
 import nl.utwente.groove.gui.list.SearchResult;
 import nl.utwente.groove.gui.tree.LabelTree;
-import nl.utwente.groove.gui.tree.LabelTree.LabelTreeNode;
+import nl.utwente.groove.gui.tree.TypeTree.TypeTreeNode;
 
 /**
  * Action for changing one label into another throughout the grammar.
@@ -86,8 +86,10 @@ public void execute() {
                     try {
                         getSimulatorModel().doRelabel(result.from(), result.to());
                     } catch (IOException exc) {
-                        showErrorDialog(exc, String.format("Error while renaming '%s' into '%s':",
-                                                           result.from(), result.to()));
+                        showErrorDialog(exc,
+                                        String
+                                            .format("Error while renaming '%s' into '%s':",
+                                                    result.from(), result.to()));
                     }
                 }
             }
@@ -116,9 +118,8 @@ public void valueChanged(TreeSelectionEvent e) {
         TreePath[] selection = ((LabelTree<?>) e.getSource()).getSelectionPaths();
         if (selection != null && selection.length > 0) {
             Object treeNode = selection[0].getLastPathComponent();
-            if (treeNode instanceof LabelTreeNode en
-                && en.getEntry().getLabel() instanceof TypeLabel tl) {
-                this.oldLabel = tl;
+            if (treeNode instanceof TypeTreeNode en) {
+                this.oldLabel = en.getEntry().getType().label();
             }
         }
     }

diff --git a/src/main/java/nl/utwente/groove/gui/action/SelectColorAction.java b/src/main/java/nl/utwente/groove/gui/action/SelectColorAction.java
@@ -20,7 +20,6 @@
 import nl.utwente.groove.grammar.model.ResourceKind;
 import nl.utwente.groove.grammar.type.TypeLabel;
 import nl.utwente.groove.grammar.type.TypeNode;
-import nl.utwente.groove.graph.EdgeRole;
 import nl.utwente.groove.graph.GraphRole;
 import nl.utwente.groove.graph.Label;
 import nl.utwente.groove.gui.Options;
@@ -30,7 +29,7 @@
 import nl.utwente.groove.gui.jgraph.JCell;
 import nl.utwente.groove.gui.jgraph.JGraph;
 import nl.utwente.groove.gui.tree.LabelTree;
-import nl.utwente.groove.gui.tree.LabelTree.LabelTreeNode;
+import nl.utwente.groove.gui.tree.TypeTree.TypeTreeNode;
 import nl.utwente.groove.util.Exceptions;
 import nl.utwente.groove.util.parse.FormatException;
 
@@ -91,13 +90,9 @@ private void checkLabelTree(LabelTree<?> tree) {
         if (selection != null) {
             for (TreePath path : selection) {
                 Object treeNode = path.getLastPathComponent();
-                if (treeNode instanceof LabelTreeNode) {
-                    Label selectedLabel = ((LabelTreeNode) treeNode).getEntry().getLabel();
-                    if (selectedLabel instanceof TypeLabel
-                        && selectedLabel.getRole() == EdgeRole.NODE_TYPE) {
-                        this.label = (TypeLabel) selectedLabel;
-                        break;
-                    }
+                if (treeNode instanceof TypeTreeNode n && n.getEntry().isForNode()) {
+                    this.label = n.getEntry().getType().label();
+                    break;
                 }
             }
         }

diff --git a/src/main/java/nl/utwente/groove/gui/menu/ShowHideMenu.java b/src/main/java/nl/utwente/groove/gui/menu/ShowHideMenu.java
@@ -27,6 +27,7 @@
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.Iterator;
+import java.util.Map;
 import java.util.Set;
 
 import javax.swing.AbstractAction;
@@ -51,6 +52,7 @@
 import nl.utwente.groove.gui.jgraph.JGraph;
 import nl.utwente.groove.gui.jgraph.LTSJCell;
 import nl.utwente.groove.gui.jgraph.LTSJGraph;
+import nl.utwente.groove.gui.tree.LabelFilter;
 import nl.utwente.groove.io.FileType;
 import nl.utwente.groove.io.GrooveFileChooser;
 import nl.utwente.groove.io.HTMLConverter;
@@ -221,13 +223,6 @@ protected ShowHideAction<G> createFromFileAction(int showMode) {
         return new TraceAction((LTSJGraph) this.jgraph, showMode);
     }
 
-    /**
-     * Factory method for <tt>LabelAction</tt>s.
-     */
-    protected ShowHideAction<G> createLabelAction(int showMode, Label label) {
-        return new LabelAction<>(this.jgraph, showMode, label);
-    }
-
     /**
      * Factory method for the label sub-menu. To be overiden, e.g., if the cell
      * labels should be adapted.
@@ -492,18 +487,16 @@ static protected class LabelAction<G extends @NonNull Graph> extends ShowHideAct
          * label.
          * @param jgraph the jgraph upon which this action works
          * @param showMode the show mode for this action
-         * @param label the label on which this action should test; may not be
-         *        <tt>null</tt>
-         * @throws IllegalArgumentException if <tt>cell</tt> does not give rise
-         *         to a valid label, i.e., <tt>getLabel(cell) == null</tt>
+         * @param entry the label on which this action should test
          */
         protected LabelAction(JGraph<G> jgraph, int showMode,
-                              Label label) throws IllegalArgumentException {
+                              Map.Entry<LabelFilter.Entry,Set<JCell<G>>> entry) throws IllegalArgumentException {
             super(jgraph, showMode, "");
-            putValue(NAME, label.text().length() == 0
+            var key = entry.getKey();
+            putValue(NAME, key.toString().isEmpty()
                 ? Options.EMPTY_LABEL_TEXT
-                : HTMLConverter.HTML_TAG.on(label.toLine().toHTMLString()));
-            this.label = label;
+                : HTMLConverter.HTML_TAG.on(key.getLine().toHTMLString()));
+            this.cells = entry.getValue();
         }
 
         /**
@@ -512,15 +505,13 @@ protected LabelAction(JGraph<G> jgraph, int showMode,
          */
         @Override
         protected boolean isInvolved(JCell<G> cell) {
-            // return getLabel(cell) != null && getLabel(cell).equals(label) ==
-            // include;
-            return cell.getKeys().contains(this.label);
+            return this.cells.contains(cell);
         }
 
         /**
          * The label on which this action selects.
          */
-        private final Label label;
+        private final Set<JCell<G>> cells;
     }
 
     /**
@@ -751,8 +742,8 @@ public void menuSelectionChanged(boolean isIncluded) {
             if (isIncluded) {
                 // now (re-)fill the menu
                 removeAll();
-                for (Label labelAction : getJGraph().getLabelTree().getLabels()) {
-                    add(new LabelAction<>(getJGraph(), this.showMode, labelAction));
+                for (var entry : getJGraph().getLabelTree().getLabels().entrySet()) {
+                    add(new LabelAction<>(getJGraph(), this.showMode, entry));
                 }
             }
             super.menuSelectionChanged(isIncluded);

diff --git a/src/main/java/nl/utwente/groove/gui/tree/LabelFilter.java b/src/main/java/nl/utwente/groove/gui/tree/LabelFilter.java
@@ -33,6 +33,7 @@
 import nl.utwente.groove.gui.jgraph.JVertex;
 import nl.utwente.groove.gui.look.VisualKey;
 import nl.utwente.groove.util.Observable;
+import nl.utwente.groove.util.line.Line;
 
 /**
  * Class that maintains a set of filtered entries
@@ -144,6 +145,7 @@ public void clear() {
         this.jCellEntryMap.clear();
         this.entryJCellMap.clear();
         this.labelEntryMap.clear();
+        this.normalMap.clear();
     }
 
     /** Returns the set of all entries known to this filter. */
@@ -155,8 +157,15 @@ public Set<Entry> getEntries() {
     public Entry getEntry(Label key) {
         LabelEntry result = this.labelEntryMap.get(key);
         if (result == null) {
-            this.labelEntryMap.put(key, result = new LabelEntry(key));
-            addEntry(result);
+            result = new LabelEntry(key);
+            // normalise the new entry
+            if (this.normalMap.containsKey(result)) {
+                result = this.normalMap.get(result);
+            } else {
+                this.normalMap.put(result, result);
+                addEntry(result);
+            }
+            this.labelEntryMap.put(key, result);
         }
         return result;
     }
@@ -167,7 +176,7 @@ public Entry getEntry(Label key) {
     void addEntry(Entry entry) {
         var old = this.entryJCellMap.put(entry, new HashSet<>());
         assert old == null : "Duplicate label entry for %s (existing entry contained %s)"
-            .formatted(entry.getLabel(), old);
+            .formatted(entry, old);
     }
 
     /** Mapping from entries to {@link JCell}s with that entry. */
@@ -176,6 +185,8 @@ void addEntry(Entry entry) {
     private final Map<JCell<G>,Set<Entry>> jCellEntryMap = new HashMap<>();
     /** Mapping from known labels to corresponding label entries. */
     private final Map<Label,LabelEntry> labelEntryMap = new HashMap<>();
+    /** Identity mapping for normalised entries. */
+    private final Map<LabelEntry,LabelEntry> normalMap = new HashMap<>();
 
     /** Convenience method to return the JCells for a given label.
      * @see #getEntry(Label)
@@ -190,7 +201,7 @@ public Set<JCell<G>> getJCells(Label label) {
      * @see #getJCells(Entry)
      */
     public boolean hasJCells(Label label) {
-        return !getJCells(getEntry(label)).isEmpty();
+        return !getJCells(label).isEmpty();
     }
 
     /**
@@ -308,8 +319,8 @@ public boolean isIncluded(JCell<G> jCell) {
 
     /** Type of the keys in a label filter. */
     public static interface Entry extends Comparable<Entry> {
-        /** Retrieves the label of the entry. */
-        public Label getLabel();
+        /** Retrieves the line of the entry. */
+        public Line getLine();
 
         /** Indicates if this entry is currently selected. */
         public boolean isSelected();
@@ -334,28 +345,34 @@ public default boolean isPassive() {
     public static class LabelEntry implements Entry {
         /** Constructs an initially selected fresh label entry from a given label. */
         public LabelEntry(Label label) {
-            this.label = label;
+            this.line = label.toLine();
+            this.role = label.getRole();
             this.selected = true;
         }
 
         @Override
-        public Label getLabel() {
-            return this.label;
+        public Line getLine() {
+            return this.line;
         }
 
+        /** The label wrapped in this entry. */
+        private final Line line;
+
         @Override
         public boolean isForNode() {
-            return getLabel().getRole() == EdgeRole.NODE_TYPE;
+            return this.role == EdgeRole.NODE_TYPE;
         }
 
+        private final EdgeRole role;
+
         @Override
         public boolean isSelected() {
             return this.selected;
         }
 
         @Override
         public boolean setSelected(boolean selected) {
-            boolean result = this.selected == selected;
+            boolean result = this.selected != selected;
             this.selected = selected;
             return result;
         }
@@ -365,13 +382,17 @@ public boolean setSelected(boolean selected) {
 
         @Override
         public int compareTo(Entry o) {
-            assert o instanceof LabelEntry;
-            return getLabel().compareTo(o.getLabel());
+            var other = (LabelEntry) o;
+            var result = this.role.compareTo(other.role);
+            if (result == 0) {
+                result = toString().compareTo(other.toString());
+            }
+            return result;
         }
 
         @Override
         public int hashCode() {
-            return this.label.getRole().hashCode() ^ this.label.text().hashCode();
+            return this.role.hashCode() ^ this.line.hashCode();
         }
 
         @Override
@@ -382,25 +403,21 @@ public boolean equals(Object obj) {
             if (obj == null) {
                 return false;
             }
-            if (!(obj instanceof LabelEntry)) {
+            if (!(obj instanceof LabelEntry other)) {
                 return false;
             }
-            Label otherLabel = ((LabelEntry) obj).getLabel();
-            if (getLabel().getRole() != otherLabel.getRole()) {
+            if (this.role != other.role) {
                 return false;
             }
-            if (!getLabel().text().equals(otherLabel.text())) {
+            if (!toString().equals(other.toString())) {
                 return false;
             }
             return true;
         }
 
         @Override
         public String toString() {
-            return this.label.toString();
+            return this.line.toFlatString();
         }
-
-        /** The label wrapped in this entry. */
-        private final Label label;
     }
 }
diff --git a/src/main/java/nl/utwente/groove/gui/tree/LabelTree.java b/src/main/java/nl/utwente/groove/gui/tree/LabelTree.java
@@ -29,7 +29,8 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
-import java.util.SortedSet;
+import java.util.SortedMap;
+import java.util.TreeMap;
 import java.util.TreeSet;
 
 import javax.swing.AbstractAction;
@@ -186,10 +187,10 @@ public boolean isFiltering() {
      * Returns the set of labels maintained by this label
      * tree.
      */
-    public SortedSet<Label> getLabels() {
-        TreeSet<Label> result = new TreeSet<>();
+    public SortedMap<Entry,Set<JCell<G>>> getLabels() {
+        TreeMap<Entry,Set<JCell<G>>> result = new TreeMap<>();
         for (Entry entry : getFilter().getEntries()) {
-            result.add(entry.getLabel());
+            result.put(entry, getFilter().getJCells(entry));
         }
         return result;
     }
@@ -448,16 +449,16 @@ public String convertValueToText(@Nullable Object value, boolean selected, boole
      */
     protected StringBuilder getText(Entry entry) {
         StringBuilder result = new StringBuilder();
-        Label label = entry.getLabel();
+        var line = entry.getLine();
         boolean specialLabelColour = false;
-        if (label.equals(TypeLabel.NODE)) {
+        if (line.toFlatString().equals(TypeLabel.NODE_LABEL_TEXT)) {
             result.append(Options.NO_LABEL_TEXT);
             specialLabelColour = true;
-        } else if (label.text().length() == 0) {
+        } else if (entry.toString().isEmpty()) {
             result.append(Options.EMPTY_LABEL_TEXT);
             specialLabelColour = true;
         } else {
-            result.append(label.toLine().toHTMLString());
+            result.append(line.toHTMLString());
         }
         if (specialLabelColour) {
             HTMLConverter.createColorTag(SPECIAL_COLOR).on(result);