diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 9fa5efc461f..1acbc33aed4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/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 showSourceViewTooltips = createBooleanProperty(SOURCE_VIEW_TOOLTIP, true); + private final PropertyEntry showProofTreeTooltips = + createBooleanProperty(PROOF_TREE_TOOLTIP, true); private final PropertyEntry highlightOrigin = createBooleanProperty(HIGHLIGHT_ORIGIN, true); private final PropertyEntry> 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(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 4863623dce8..870acc2b682 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/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; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java new file mode 100644 index 00000000000..fdc1637ab10 --- /dev/null +++ b/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); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java index 9e83ad4c04e..057bf1fc44c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java +++ b/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. * diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 5ccd3abc9fc..45fe758240f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/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() {