diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index 9bb8c690572..4c7b5022822 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java @@ -85,7 +85,7 @@ public class NodeInfo { private boolean uselessApplication = false; /** User-provided plain-text annotations to the node. */ - private String notes; + private @Nullable String notes; /** Information about changes respective to the parent of this node. */ private SequentChangeInfo sequentChangeInfo; @@ -476,7 +476,7 @@ public boolean getScriptRuleApplication() { * * @param newNotes annotations as described above */ - public void setNotes(String newNotes) { + public void setNotes(@Nullable String newNotes) { String oldNotes = notes; notes = newNotes; if (!Objects.equals(oldNotes, newNotes)) { @@ -489,7 +489,7 @@ public void setNotes(String newNotes) { * * @return annotations as described above */ - public String getNotes() { + public @Nullable String getNotes() { return notes; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java index d559241955f..03f1b763197 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java @@ -116,6 +116,27 @@ public synchronized void setSelectedNode(Node n) { fireSelectedNodeChanged(previousSelectedNode); } + /// Selects the node with the given serial number, if it exists in the current proof. + /// @param serialNr the serial number of the node to select + /// @return true if the node was found and selected, false otherwise + public synchronized boolean setSelectedNodeBySerialNr(int serialNr) { + final Node previousSelectedNode = selectedNode; + if (proof == null) { + return false; + } + Node node = proof.findAny(n -> n.serialNr() == serialNr); + if (node == null) { + return false; + } + goalIsValid = false; + selectedNode = node; + selectedSequent = selectedNode.sequent(); + selectedRuleApp = selectedNode.getAppliedRuleApp(); + setSelectedNode(node); + fireSelectedNodeChanged(previousSelectedNode); + return true; + } + /** * Sets the node and sequent focused by the user. * 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 e634062eed4..70c71dbc08c 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 @@ -1118,6 +1118,7 @@ public void menuCanceled(MenuEvent e) { if (selected == null) { proof.addSeparator(); proof.add(new SearchInProofTreeAction(this)); + proof.add(new GotoNodeAction(this)); proof.add(new SearchInSequentAction(this, sequentViewSearchBar)); proof.add(new SearchNextAction(this, sequentViewSearchBar)); proof.add(new SearchPreviousAction(this, sequentViewSearchBar)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GotoNodeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GotoNodeAction.java new file mode 100644 index 00000000000..15c2ab9eb4e --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GotoNodeAction.java @@ -0,0 +1,30 @@ +/* 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 de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.fonticons.IconFactory; + +/// Menu option for selecting the proof node with the given node number. +/// +/// Keyboard shortcut: Ctrl + G (see {@link de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeSettings}) +/// +/// @author Wolfram Pfeifer +public class GotoNodeAction extends MainWindowAction { + + public GotoNodeAction(MainWindow mainWindow) { + super(mainWindow); + setName("Go to Node..."); + setIcon(IconFactory.GOTO_NODE.get(IconFactory.DEFAULT_SIZE)); + setTooltip("Go to the proof node with the given node number."); + getMediator().enableWhenProofLoaded(this); + } + + @Override + public void actionPerformed(ActionEvent arg0) { + mainWindow.getProofTreeView().showGotoNodeDialog(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java index d3503a96fcc..0d70b1b96da 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java @@ -158,6 +158,8 @@ public final class IconFactory { new IconFontProvider(FontAwesomeSolid.ARROW_LEFT); public static final IconFontProvider ORIGIN_LABELS = new IconFontProvider(FontAwesomeSolid.ROUTE); + public static final IconFontProvider GOTO_NODE = + new IconFontProvider(FontAwesomeSolid.CROSSHAIRS); private static final Logger LOGGER = LoggerFactory.getLogger(IconFactory.class); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index 0cdfefc4741..dd0c17a4f82 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -99,6 +99,7 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { // defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK); defineDefault(OpenFileAction.class, KeyEvent.VK_O, SHORTCUT_KEY_MASK); defineDefault(SearchInSequentAction.class, KeyEvent.VK_F, SHORTCUT_KEY_MASK); + defineDefault(GotoNodeAction.class, KeyEvent.VK_G, SHORTCUT_KEY_MASK); // "special" keystrokes defineDefault(SearchNextAction.class, KeyEvent.VK_F3, 0); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index 9077e2d5259..0594df73dbe 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -347,7 +347,7 @@ public void actionPerformed(ActionEvent e) { static class Notes extends ProofTreeAction { public Notes(ProofTreeContext context) { super(context); - setName("Edit Notes..."); + setName("Set bookmark/Annotate ..."); setIcon(IconFactory.editFile(ICON_SIZE)); } @@ -355,7 +355,10 @@ public Notes(ProofTreeContext context) { public void actionPerformed(ActionEvent e) { // display a dialog to attach text to the node final Icon editIcon = IconFactory.editFile(20); - final String origNotes = context.invokedNode.getNodeInfo().getNotes(); + String origNotes = context.invokedNode.getNodeInfo().getNotes(); + if (origNotes == null || origNotes.isBlank()) { + origNotes = "Bookmark %d".formatted(context.invokedNode.serialNr()); + } final String newNotes = (String) JOptionPane.showInputDialog(context.proofTreeView, null, "Annotate this proof node", JOptionPane.PLAIN_MESSAGE, editIcon, null, origNotes); 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 e03c4680f8c..0c3894b1056 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 @@ -4,6 +4,7 @@ package de.uka.ilkd.key.gui.prooftree; import java.util.function.Supplier; +import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.docking.DynamicCMenu; @@ -36,6 +37,7 @@ public static CAction create(ProofTreeView view) { CMenu menu = new CMenu(); menu.add(createSearch(view)); + menu.add(createGotoNode(view)); menu.addSeparator(); menu.add(createExpandAll(view)); @@ -89,6 +91,14 @@ private static CButton createSearch(ProofTreeView view) { return button; } + private static CButton createGotoNode(ProofTreeView view) { + CButton button = new CButton(); + button.setText("Go to Node..."); + button.setIcon(IconFactory.GOTO_NODE.get(IconFactory.DEFAULT_SIZE)); + button.addActionListener(e -> view.showGotoNodeDialog()); + return button; + } + private static CButton createCollapseAll(ProofTreeView view) { CButton button = new CButton(); button.setText("Collapse All"); 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 8e5bb4ea167..bf5c5e66070 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 @@ -848,6 +848,151 @@ public void showSearchPanel() { proofTreeSearchPanel.setVisible(true); } + public void showGotoNodeDialog() { + // Build a combined dialog that allows direct input of a node number and shows all nodes + // annotated with notes in a JList. If there are no notes, show the explanatory message. + + final var currentProof = mediator != null ? mediator.getSelectedProof() : null; + + // Top: input panel for direct node number entry (keeps existing functionality) + final var inputLabel = new JLabel("Node number:"); + final var inputField = new JTextField(); + inputField.setColumns(10); + final var inputPanel = new JPanel(new BorderLayout(8, 0)); + inputPanel.add(inputLabel, BorderLayout.WEST); + inputPanel.add(inputField, BorderLayout.CENTER); + + // Center: either noted-nodes list or explanatory message + final JComponent centerComponent; + final JList notedList; + // Collect nodes with notes (global) + final java.util.List notedNodes = new ArrayList<>(); + for (Iterator it = currentProof.root().subtreeIterator(); it.hasNext();) { + final Node n = it.next(); + final String notes = n.getNodeInfo().getNotes(); + if (notes != null) { + notedNodes.add(n); + } + } + notedNodes.sort(Comparator.comparingInt(Node::serialNr)); + + if (!notedNodes.isEmpty()) { + notedList = new JList<>(notedNodes.toArray(new Node[0])); + notedList.setVisibleRowCount(Math.min(8, notedNodes.size())); + notedList.setSelectionMode(ListSelectionModel.SINGLE_SELECTION); + // Custom renderer: ": " on first line, first line of note below + notedList.setCellRenderer(new DefaultListCellRenderer() { + @Override + public Component getListCellRendererComponent(JList list, Object value, + int index, boolean isSelected, boolean cellHasFocus) { + final Component c = super.getListCellRendererComponent(list, value, index, + isSelected, cellHasFocus); + if (value instanceof Node n) { + final var app = n.getAppliedRuleApp(); + final String ruleName = app != null + ? app.rule().name().toString() + : "Root"; + String note = n.getNodeInfo().getNotes(); + if (note == null) + note = ""; + int nl = note.indexOf('\n'); + final String firstLine = nl >= 0 ? note.substring(0, nl) : note; + // Limit overly long lines for display + final String firstLineShort = firstLine.length() > 40 + ? firstLine.substring(0, 40) + " …" + : firstLine; + // Use simple HTML for two-line display + final String html = "" + n.serialNr() + ": " + + LogicPrinter.escapeHTML(ruleName, true) + + "
" + LogicPrinter.escapeHTML(firstLineShort, true); + ((JLabel) c).setText(html); + c.setFont(UIManager.getFont("TextArea.font")); + ((JLabel) c).setIcon(IconFactory.editFile(16)); + } + return c; + } + }); + centerComponent = new JScrollPane(notedList); + } else { + notedList = null; + final var info = new JLabel( + "Nodes that have been bookmarked using
" + + "the node context menu will be listed here."); + info.setFont(UIManager.getFont("TextArea.font")); + centerComponent = info; + centerComponent.setBorder( + BorderFactory.createEmptyBorder(6, 0, 0, 0)); + } + + + final var panel = new JPanel(new BorderLayout(0, 8)); + panel.add(inputPanel, BorderLayout.NORTH); + panel.add(centerComponent, BorderLayout.CENTER); + + final var optionPane = new JOptionPane(panel, JOptionPane.PLAIN_MESSAGE, + JOptionPane.OK_CANCEL_OPTION, IconFactory.GOTO_NODE.get(IconFactory.DEFAULT_SIZE)); + final var dialog = optionPane.createDialog(this, "Go to proof node"); + + // Ensure the input field has focus once the dialog is shown + dialog.addWindowFocusListener(new WindowAdapter() { + @Override + public void windowGainedFocus(WindowEvent e) { + inputField.requestFocusInWindow(); + } + }); + + // Allow double-click on a list entry to immediately jump and close the dialog + if (notedList != null) { + notedList.addMouseListener(new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + final Node sel = notedList.getSelectedValue(); + if (sel != null) { + if (e.getClickCount() == 2) { + mediator.getSelectionModel().setSelectedNode(sel); + dialog.dispose(); + } + if (e.getClickCount() == 1) { + inputField.setText(Integer.toString(sel.serialNr())); + } + } + } + }); + } + + inputField.requestFocus(); + dialog.setVisible(true); + + final Object chosen = optionPane.getValue(); + if (!(chosen instanceof Integer) || ((Integer) chosen) != JOptionPane.OK_OPTION) { + return; // cancelled or closed + } + + // OK pressed: prefer list selection; otherwise parse number field + if (notedList != null) { + final Node sel = notedList.getSelectedValue(); + if (sel != null) { + mediator.getSelectionModel().setSelectedNode(sel); + return; + } + } + + inputField.requestFocus(); + final String nodeStr = inputField.getText(); + if (nodeStr != null && !nodeStr.isEmpty()) { + try { + int serialNr = Integer.parseUnsignedInt(nodeStr); + if (!getMediator().getSelectionModel().setSelectedNodeBySerialNr(serialNr)) { + JOptionPane.showMessageDialog(this, "Node not found: " + nodeStr, + "Error", JOptionPane.ERROR_MESSAGE); + } + } catch (NumberFormatException ex) { + JOptionPane.showMessageDialog(this, "Invalid node number: " + nodeStr, + "Error", JOptionPane.ERROR_MESSAGE); + } + } + } + /** * Expands all currently visible nodes. Used by the collapsing search to reveal the (few) * surviving matching nodes after the tree has been filtered down to them.