Resolved gh issue #786 & preparing release 6.9.1

release/include/CHANGES.md

@@ -3,6 +3,11 @@ GROOVE Change Log
 
 This document describes the major changes in the GROOVE tool set
 
+Release 6.9.1, 1 August 2024
+-------------------------------
+- Hugely improved behaviour of (label and) type tree (gh issue #786)
+- Bug fixes: GH issues #796, #797
+
 Release 6.9.0, 20 July 2024
 -------------------------------
 - Added .dot export as well as .gcp export for LTSs

src/main/java/nl/utwente/groove/gui/Icons.java

@@ -25,10 +25,12 @@
 import java.awt.Point;
 import java.awt.Toolkit;
 
+import javax.swing.Icon;
 import javax.swing.ImageIcon;
 
 import nl.utwente.groove.grammar.QualName;
 import nl.utwente.groove.grammar.model.ResourceKind;
+import nl.utwente.groove.gui.tree.CheckBoxPassiveIcon;
 import nl.utwente.groove.io.store.EditType;
 
 /**
@@ -210,6 +212,8 @@ public static ImageIcon getListIcon(ResourceKind resource) {
     public static final ImageIcon ARROW_SIMPLE_UP_ICON = createIcon("arrow-simple-up.gif");
     /** Cancel action icon. */
     public static final ImageIcon CANCEL_ICON = createIcon("cancel.gif");
+    /** Selected checkbox. */
+    public static final Icon CHECKBOX_PASSIVE_ICON = CheckBoxPassiveIcon.instance();
     /** Compass icon. */
     public static final ImageIcon COMPASS_ICON = createIcon("compass.gif");
     /** Control automaton preview icon. */

src/main/java/nl/utwente/groove/gui/Options.java

@@ -60,8 +60,10 @@
 import javax.swing.event.ChangeListener;
 import javax.swing.plaf.metal.MetalLookAndFeel;
 
+import org.eclipse.jdt.annotation.NonNull;
 import org.jgraph.graph.GraphConstants;
 
+import com.jgoodies.looks.plastic.PlasticLookAndFeel;
 import com.jgoodies.looks.plastic.theme.DesertBlue;
 
 import nl.utwente.groove.grammar.QualName;
@@ -92,7 +94,6 @@ public Options() {
         addCheckbox(SHOW_STATE_STATUS_OPTION);
         addCheckbox(SHOW_CONTROL_STATE_OPTION);
         addCheckbox(SHOW_INVARIANTS_OPTION);
-        addCheckbox(SHOW_UNFILTERED_EDGES_OPTION);
         addCheckbox(SHOW_ARROWS_ON_LABELS_OPTION);
         addCheckbox(SHOW_BIDIRECTIONAL_EDGES_OPTION);
         addBehaviour(DELETE_RESOURCE_OPTION, 2);
@@ -276,14 +277,14 @@ public void stateChanged(ChangeEvent e) {
     }
 
     /** Creates a button for a given action with the right look-and-feel. */
-    static public JButton createButton(Action action) {
+    static public @NonNull JButton createButton(Action action) {
         JButton result = new JButton(action);
         setLAF(result);
         return result;
     }
 
     /** Creates a toggle button for a given action with the right look-and-feel. */
-    static public JToggleButton createToggleButton(Action action) {
+    static public @NonNull JToggleButton createToggleButton(Action action) {
         JToggleButton result = new JToggleButton(action);
         setLAF(result);
         return result;
@@ -516,12 +517,10 @@ public static String getNewResourceName(ResourceKind resource) {
     /** Export type action name */
     public static final String EXPORT_TYPE_ACTION_NAME = "Export Type ...";
     /** Export label filter action name */
-    public static final String FILTER_ACTION_NAME = "Filter labels";
-    /** Filter LTS action name */
-    public static final String FILTER_LTS_ACTION_NAME = "Filter LTS";
-    /** Export type-based label filter action name */
-    public static final String FILTER_TYPE_ACTION_NAME = "Filter type graph";
-    /** Back action name */
+    public static final String FILTE_SELECT_ACTION_NAME = "Include selected labels";
+    /** Load grammar action name */
+    public static final String FILTER_UNSELECT_ACTION_NAME = "Exclude selected labels";
+    /** Forward action name */
     public static final String FORWARD_ACTION_NAME = "Step Forward";
     /** Find a final state action name */
     public static final String GOTO_FINAL_STATE_ACTION_NAME = "Go to Final State";
@@ -537,7 +536,7 @@ public static String getNewResourceName(ResourceKind resource) {
     public static final String LOAD_START_STATE_ACTION_NAME = "Load External Start State ...";
     /** Import action name */
     public static final String IMPORT_ACTION_NAME = "Import ...";
-    /** Load grammar action name */
+    /** Unfilter labels action name */
     public static final String LOAD_GRAMMAR_ACTION_NAME = "Load Grammar ...";
     /** Load grammar from url action name */
     public static final String LOAD_URL_GRAMMAR_ACTION_NAME = "Load Grammar from URL ...";
@@ -679,8 +678,6 @@ public static final String getSaveStateActionName(boolean saveAs) {
     public static final String SYSTEM_PROPERTIES_ACTION_NAME = "Grammar Properties ...";
     /** Undo action name */
     public static final String UNDO_ACTION_NAME = "Undo";
-    /** Unfilter labels action name */
-    public static final String UNFILTER_ACTION_NAME = "Reset label filter";
     /** Unfilter type-based labels action name */
     public static final String UNFILTER_TYPE_ACTION_NAME = "Reset type graph filter";
     /** Pan mode action name */
@@ -873,8 +870,6 @@ public static final Set<ResourceKind> getOptionalTabs() {
     static public final String SHOW_ABSENT_STATES_OPTION = "Show absent states";
     /** Show recipe steps option */
     static public final String SHOW_RECIPE_STEPS_OPTION = "Show recipe steps";
-    /** Show unfiltered edges to filtered nodes. */
-    static public final String SHOW_UNFILTERED_EDGES_OPTION = "Show all unfiltered edges";
     /** Show data values as nodes rather than assignments. */
     static public final String SHOW_VALUE_NODES_OPTION = "Show data values as nodes";
     /** Show data values as nodes rather than assignments. */
@@ -903,7 +898,6 @@ public static final Set<ResourceKind> getOptionalTabs() {
         boolOptionDefaults.put(SHOW_ABSENT_STATES_OPTION, true);
         boolOptionDefaults.put(SHOW_ASPECTS_OPTION, false);
         boolOptionDefaults.put(SHOW_VALUE_NODES_OPTION, false);
-        boolOptionDefaults.put(SHOW_UNFILTERED_EDGES_OPTION, false);
         boolOptionDefaults.put(SHOW_ARROWS_ON_LABELS_OPTION, false);
         boolOptionDefaults.put(SHOW_BIDIRECTIONAL_EDGES_OPTION, true);
         intOptionDefaults.put(DELETE_RESOURCE_OPTION, BehaviourOption.ASK);
@@ -1016,7 +1010,7 @@ public static void initLookAndFeel() {
                 // go here
                 MetalLookAndFeel.setCurrentTheme(new DesertBlue());
                 // Set the look and feel
-                UIManager.setLookAndFeel(new com.jgoodies.looks.plastic.PlasticLookAndFeel());
+                UIManager.setLookAndFeel(new PlasticLookAndFeel());
             } catch (Exception e) {
                 throw new IllegalStateException(e);
             }

src/main/java/nl/utwente/groove/gui/Simulator.java

@@ -29,7 +29,6 @@
 import static nl.utwente.groove.gui.Options.SHOW_RECIPE_STEPS_OPTION;
 import static nl.utwente.groove.gui.Options.SHOW_STATE_IDS_OPTION;
 import static nl.utwente.groove.gui.Options.SHOW_STATE_STATUS_OPTION;
-import static nl.utwente.groove.gui.Options.SHOW_UNFILTERED_EDGES_OPTION;
 import static nl.utwente.groove.gui.Options.SHOW_VALUE_NODES_OPTION;
 import static nl.utwente.groove.gui.Options.VERIFY_ALL_STATES_OPTION;
 import static nl.utwente.groove.io.FileType.GRAMMAR;
@@ -673,7 +672,6 @@ private JMenu createOptionsMenu() {
             result.add(getOptions().getItem(SHOW_ANCHORS_OPTION));
             result.add(getOptions().getItem(SHOW_ASPECTS_OPTION));
             result.add(getOptions().getItem(SHOW_VALUE_NODES_OPTION));
-            result.add(getOptions().getItem(SHOW_UNFILTERED_EDGES_OPTION));
             result.add(getOptions().getItem(SHOW_BIDIRECTIONAL_EDGES_OPTION));
             result.add(getOptions().getItem(SHOW_ARROWS_ON_LABELS_OPTION));
             break;

src/main/java/nl/utwente/groove/gui/action/ExportAction.java

@@ -88,7 +88,8 @@ private String getActionName() {
         String type = null;
         if (this.isGraph) {
             JGraph<?> jGraph = getJGraph();
-            Graph graph = jGraph.getModel().getGraph();
+            Graph graph = jGraph.getGraph();
+            assert graph != null;
             GraphRole role = graph.getRole();
             boolean isState = jGraph instanceof AspectJGraph ag && ag.isForState();
             type = isState

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.EntryNode;
+import nl.utwente.groove.gui.tree.LabelTree.LabelTreeNode;
 
 /**
  * Action for changing one label into another throughout the grammar.
@@ -116,7 +116,7 @@ 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 EntryNode en
+            if (treeNode instanceof LabelTreeNode en
                 && en.getEntry().getLabel() instanceof TypeLabel tl) {
                 this.oldLabel = tl;
             }

src/main/java/nl/utwente/groove/gui/action/LayoutAction.java

@@ -1,17 +1,17 @@
 /*
  * GROOVE: GRaphs for Object Oriented VErification Copyright 2003--2023
  * University of Twente
- * 
+ *
  * Licensed under the Apache License, Version 2.0 (the "License"); you may not
  * use this file except in compliance with the License. You may obtain a copy of
  * the License at http://www.apache.org/licenses/LICENSE-2.0
- * 
+ *
  * Unless required by applicable law or agreed to in writing, software
  * distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
  * WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
  * License for the specific language governing permissions and limitations under
  * the License.
- * 
+ *
  * $Id$
  */
 package nl.utwente.groove.gui.action;
@@ -53,7 +53,9 @@ public void actionPerformed(ActionEvent e) {
     public void doLayout() {
         // only layout selected cells, if there are any
         Object[] selection = this.jGraph.getSelectionCells();
-        this.jGraph.getModel().setLayoutable(selection.length == 0);
+        var jModel = this.jGraph.getModel();
+        assert jModel != null;
+        jModel.setLayoutable(selection.length == 0);
         for (Object jCell : selection) {
             if (jCell instanceof JVertex) {
                 ((JVertex<?>) jCell).setLayoutable(true);

src/main/java/nl/utwente/groove/gui/action/SelectColorAction.java

@@ -30,7 +30,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.EntryNode;
+import nl.utwente.groove.gui.tree.LabelTree.LabelTreeNode;
 import nl.utwente.groove.util.Exceptions;
 import nl.utwente.groove.util.parse.FormatException;
 
@@ -91,8 +91,8 @@ private void checkLabelTree(LabelTree<?> tree) {
         if (selection != null) {
             for (TreePath path : selection) {
                 Object treeNode = path.getLastPathComponent();
-                if (treeNode instanceof EntryNode) {
-                    Label selectedLabel = ((EntryNode) treeNode).getEntry().getLabel();
+                if (treeNode instanceof LabelTreeNode) {
+                    Label selectedLabel = ((LabelTreeNode) treeNode).getEntry().getLabel();
                     if (selectedLabel instanceof TypeLabel
                         && selectedLabel.getRole() == EdgeRole.NODE_TYPE) {
                         this.label = (TypeLabel) selectedLabel;

src/main/java/nl/utwente/groove/gui/dialog/GraphPreviewDialog.java

@@ -16,6 +16,8 @@
 import javax.swing.SwingUtilities;
 import javax.swing.WindowConstants;
 
+import org.eclipse.jdt.annotation.NonNull;
+
 import nl.utwente.groove.control.graph.ControlGraph;
 import nl.utwente.groove.grammar.aspect.GraphConverter;
 import nl.utwente.groove.grammar.model.GrammarModel;
@@ -36,7 +38,7 @@
  * Dialog showing an given graph in the most appropriate
  * GUI component.
  */
-public class GraphPreviewDialog<G extends Graph> extends JDialog {
+public class GraphPreviewDialog<G extends @NonNull Graph> extends JDialog {
     /** Constructs a new dialog, for a given graph. */
     public GraphPreviewDialog(GrammarModel grammar, G graph) {
         this(null, grammar, graph);

src/main/java/nl/utwente/groove/gui/display/DismissDelayer.java

@@ -26,7 +26,7 @@
  * Mouse listener that will set the tool tip dismiss delay to
  * infinite whenever a given component is entered.
  */
-public final class DismissDelayer extends MouseAdapter {
+public class DismissDelayer extends MouseAdapter {
     /**
      * Constructs a delayer for a given component.
      * @param component the component on which this mouse listener works.

src/main/java/nl/utwente/groove/gui/display/DisplaysPanel.java

@@ -44,7 +44,6 @@
 import nl.utwente.groove.grammar.QualName;
 import nl.utwente.groove.grammar.model.GrammarModel;
 import nl.utwente.groove.grammar.model.ResourceKind;
-import nl.utwente.groove.gui.LongToolTipAdapter;
 import nl.utwente.groove.gui.Options;
 import nl.utwente.groove.gui.Simulator;
 import nl.utwente.groove.gui.SimulatorListener;
@@ -156,7 +155,7 @@ public void itemStateChanged(ItemEvent e) {
             });
         }
         this.simulator.getModel().addListener(this, Change.DISPLAY, Change.GRAMMAR);
-        getUpperListsPanel().addMouseListener(new LongToolTipAdapter(getUpperListsPanel()));
+        getUpperListsPanel().addMouseListener(new DismissDelayer(getUpperListsPanel()));
         activateListeners();
     }