Option to disable ProofTree tooltips, render them lazily (#3510)

key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java

@@ -112,6 +112,9 @@ public class ViewSettings extends AbstractPropertiesSettings {
     /** this setting enables/disables tool tips in the source view */
     private static final String SOURCE_VIEW_TOOLTIP = "SourceViewTooltips";
 
+    /** this setting enables/disables tool tips in the proof tree */
+    private static final String PROOF_TREE_TOOLTIP = "ProofTreeTooltips";
+
     private static final String HIGHLIGHT_ORIGIN = "HighlightOrigin";
     /**
      *
@@ -202,6 +205,8 @@ public class ViewSettings extends AbstractPropertiesSettings {
         createBooleanProperty(SEQUENT_VIEW_TOOLTIP, true);
     private final PropertyEntry<Boolean> showSourceViewTooltips =
         createBooleanProperty(SOURCE_VIEW_TOOLTIP, true);
+    private final PropertyEntry<Boolean> showProofTreeTooltips =
+        createBooleanProperty(PROOF_TREE_TOOLTIP, true);
     private final PropertyEntry<Boolean> highlightOrigin =
         createBooleanProperty(HIGHLIGHT_ORIGIN, true);
     private final PropertyEntry<Set<String>> clutterRules =
@@ -539,6 +544,14 @@ public void setShowSourceViewTooltips(boolean showSourceViewTooltips) {
         this.showSourceViewTooltips.set(showSourceViewTooltips);
     }
 
+    public boolean isShowProofTreeTooltips() {
+        return showProofTreeTooltips.get();
+    }
+
+    public void setShowProofTreeTooltips(boolean showProofTreeTooltips) {
+        this.showProofTreeTooltips.set(showProofTreeTooltips);
+    }
+
     public double getUIFontSizeFactor() {
         return uiFontSizeFactor.get();
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -164,6 +164,8 @@ public final class MainWindow extends JFrame {
         new ToggleSequentViewTooltipAction(this);
     private final ToggleSourceViewTooltipAction toggleSourceViewTooltipAction =
         new ToggleSourceViewTooltipAction(this);
+    private final ToggleProofTreeTooltipAction toogleProofTreeTooltipAction =
+        new ToggleProofTreeTooltipAction(this);
     private final TermLabelMenu termLabelMenu;
     private boolean frozen = false;
     /**
@@ -930,6 +932,7 @@ private JMenu createViewMenu() {
         view.add(new JCheckBoxMenuItem(hidePackagePrefixToggleAction));
         view.add(new JCheckBoxMenuItem(toggleSequentViewTooltipAction));
         view.add(new JCheckBoxMenuItem(toggleSourceViewTooltipAction));
+        view.add(new JCheckBoxMenuItem(toogleProofTreeTooltipAction));
 
         view.addSeparator();
         {
@@ -1457,6 +1460,11 @@ public boolean isShowTacletInfo() {
         return mainFrame.isShowTacletInfo();
     }
 
+    public void setShowProofTreeTooltip(Object source) {
+        toogleProofTreeTooltipAction
+                .actionPerformed(new ActionEvent(proofTreeView, ActionEvent.ACTION_PERFORMED, ""));
+    }
+
     public AutoModeAction getAutoModeAction() {
         return autoModeAction;
     }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java

@@ -0,0 +1,58 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.gui.actions;
+
+import java.awt.event.ActionEvent;
+import java.beans.PropertyChangeListener;
+import javax.swing.*;
+
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import de.uka.ilkd.key.settings.ViewSettings;
+
+/**
+ * Toggles the tooltips of the proof tree.
+ *
+ * @author Wolfram Pfeifer
+ */
+public class ToggleProofTreeTooltipAction extends MainWindowAction {
+    /** This action's name. */
+    public static final String NAME = "Show Tooltips in Proof Tree";
+
+    /** This action's tooltip. */
+    public static final String TOOL_TIP = "If ticked, moving the mouse over a node in the proof"
+        + " tree will show a tooltip with additional information.";
+
+    /**
+     * Create a new action.
+     *
+     * @param mainWindow the main window.
+     */
+    public ToggleProofTreeTooltipAction(MainWindow mainWindow) {
+        super(mainWindow);
+        setName(NAME);
+        setTooltip(TOOL_TIP);
+        // Listens to changes to the view settings to call {@link #updateSelectedState()}.
+        PropertyChangeListener viewSettingsListener = e -> updateSelectedState();
+        ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
+                .addPropertyChangeListener(viewSettingsListener);
+        updateSelectedState();
+    }
+
+    /**
+     * Updates the state of this action according to {@link ViewSettings#isShowProofTreeTooltips()}
+     */
+    protected void updateSelectedState() {
+        final boolean setting =
+            ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isShowProofTreeTooltips();
+        setSelected(setting);
+    }
+
+    @Override
+    public void actionPerformed(ActionEvent e) {
+        boolean selected = ((JCheckBoxMenuItem) e.getSource()).isSelected();
+        ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
+                .setShowProofTreeTooltips(selected);
+    }
+}

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java

@@ -10,6 +10,7 @@
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 
 import bibliothek.gui.dock.common.action.CAction;
 import bibliothek.gui.dock.common.action.CButton;
@@ -39,6 +40,7 @@ public static CAction create(ProofTreeView view) {
             menu.addSeparator();
 
             menu.add(createExpandOSSToggle(view));
+            menu.add(createTooltipToggle());
             menu.add(createTacletInfoToggle());
             return menu;
         };
@@ -134,6 +136,27 @@ protected void changed() {
         return check;
     }
 
+    private static CCheckBox createTooltipToggle() {
+        CCheckBox check = new CCheckBox() {
+            @Override
+            protected void changed() {
+                /*
+                 * The ToogleProofTreeTooltipAction (in the View menu) is updated via
+                 * PropertyChangeListener, no manual update needed!
+                 */
+                final boolean selected = isSelected();
+                ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
+                        .setShowProofTreeTooltips(selected);
+            }
+        };
+        check.setText("Show Tooltips");
+        // No PropertyChangeListener needed, since the menu is always freshly generated.
+        final boolean setting =
+            ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isShowProofTreeTooltips();
+        check.setSelected(setting);
+        return check;
+    }
+
     /**
      * The checkbox used in the proof tree settings.
      *

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java

@@ -176,6 +176,35 @@ public ProofTreeView() {
         delegateView = new JTree(new DefaultMutableTreeNode("No proof loaded")) {
             private static final long serialVersionUID = 6555955929759162324L;
 
+            @Override
+            public String getToolTipText(MouseEvent mouseEvent) {
+                /*
+                 * For performance reasons, we want to make sure that the tooltips are only rendered
+                 * when they are really needed. Therefore, they are now lazily generated and can
+                 * also be disabled completely.
+                 */
+                if (!ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
+                        .isShowProofTreeTooltips()) {
+                    return null;
+                }
+                TreePath path = delegateView.getPathForLocation(mouseEvent.getX(),
+                    mouseEvent.getY());
+                if (path == null) {
+                    return null;
+                }
+                var last = path.getLastPathComponent();
+
+                if (last instanceof GUIAbstractTreeNode node) {
+
+                    Style style = renderer.initStyleForNode(node);
+                    if (style.tooltip != null) {
+                        return renderTooltip(style.tooltip);
+                    }
+                }
+
+                return super.getToolTipText(mouseEvent);
+            }
+
             @Override
             public void setFont(Font font) {
                 iconHeight = font.getSize();
@@ -1243,16 +1272,7 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean
 
             super.getTreeCellRendererComponent(tree, value, sel, expanded, leaf, row, hasFocus);
 
-            Style style = new Style();
-            style.foreground = getForeground();
-            style.background = getBackground();
-            // Normalize whitespace
-            style.text = value.toString().replaceAll("\\s+", " ");
-            style.border = null;
-            style.tooltip = new Style.Tooltip();
-            style.icon = null;
-
-            stylers.forEach(it -> it.style(style, node));
+            Style style = initStyleForNode(node);
 
             setForeground(style.foreground);
             setBackground(style.background);
@@ -1265,13 +1285,34 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean
             }
 
             setFont(getFont().deriveFont(Font.PLAIN));
-            String tooltip = renderTooltip(style.tooltip);
-            setToolTipText(tooltip);
+            // For performance reasons, we render the tooltips now lazily ...
+            // String tooltip = renderTooltip(style.tooltip);
+            // setToolTipText(tooltip);
             setText(style.text);
             setIcon(style.icon);
 
             return this;
         }
+
+        /**
+         * Creates a new Style object and fills it for the given node.
+         *
+         * @param node the tree node
+         * @return the created Style with all the info about the node
+         */
+        public Style initStyleForNode(GUIAbstractTreeNode node) {
+            Style style = new Style();
+            style.foreground = getForeground();
+            style.background = getBackground();
+            // Normalize whitespace
+            style.text = node.toString().replaceAll("\\s+", " ");
+            style.border = null;
+            style.tooltip = new Style.Tooltip();
+            style.icon = null;
+
+            stylers.forEach(it -> it.style(style, node));
+            return style;
+        }
     }
 
     public Node getSelectedNode() {