Small feature: go to node with given serial number

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;
     }
 

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.
      *

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));

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();
+    }
+}

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);
 

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);

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

@@ -347,15 +347,18 @@ 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));
         }
 
         @Override
         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);

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");

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<Node> notedList;
+        // Collect nodes with notes (global)
+        final java.util.List<Node> notedNodes = new ArrayList<>();
+        for (Iterator<Node> 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: "<serial>: <ruleName>" 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 = "<html><b>" + n.serialNr() + ": "
+                            + LogicPrinter.escapeHTML(ruleName, true)
+                            + "</b><br>" + 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(
+                "<html>Nodes that have been bookmarked using<br>" +
+                    "the node context menu will be listed here.</html>");
+            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.